LRI Équipe MODHEL Bât 650 Ada Lovelace, Université Paris Sud Rue Noetzlin, 91190 Gif-sur-Yvette, France
Isabelle club meeting on December 16 2015

# Audience

• Thibaut Balabonski
• Safouan Taha
• Yakoub Nemouchi
• Frédéric Tuong
• Burkhart Wolff
• Lina Ye

# Pearl

Benoit

## Nominals in Isabelle

### Motivation

• representations des calculs lambda, PCF ou variants avec points fixes, matching.
• modèles de machine rereduction avec d’état

Facon standard : calcul de Bruin

• dantesque
• explicit deBruin lift counterintuitive and difficult to handle
• error prone, often not feasible.
• complications in proofs

Solution: Theory of nominal types providing a built-in notion of bound variables.

### Theorie

• TYP X : “the terms”
           ([(x,y)] $λx. x) = λy. y  • TYP A : atomes “the variables" • enumerable • infini  Perm A = ensembles de permutations sur A a support fini  • OP * : Perm A × X ⇒ X " the renaming" • OP$ : Perm A × A ⇒ A " lookup"
• Properties:
    π_1 $(π_2$ x) = (π_1 o π_2) $x id$ x = x

• Interpretation of nominal type: (X, *)
     such that all (x ∈ X) are a finite support called supp(x)

• ∀ π ∈ Perm A,
• ∀ ∈ supp(x). π a = a) π $x = x ### Implementation in Isabelle/Nominal: atom_decl name nominal_datatype lam = Var name | App lam lam | Lam <<name>>. lam  This presentation in Isar syntax is internally mapped to a raw datatype. In HOL : datatype φ = PVar name | Papp (φ x φ) | PLam “name ⇒ (φ option)”  The subset π_α is defined inductively: • PVar(a) ∈ φ_α • t_1, t_2 ∈ φ_α ⟹ Papp (t_1, t_2) ∈ φ_α • a ∈ A, t ∈ φ_α ⟹ PLam [a]$t ∈ φ_α
       where

[a]$t = λ b. (if a = b then Some t else if b # t then Some(a,b)$ t
else None)


### Applications

• diverse lambda calculi,
• CCS --- with dynamic creation of channels that works ...