34 |
34 |
35 \begin{abstract} |
35 \begin{abstract} |
36 Pitts et al introduced a beautiful theory about names and binding based on the |
36 Pitts et al introduced a beautiful theory about names and binding based on the |
37 notions of atoms, permutations and support. The engineering challenge is to |
37 notions of atoms, permutations and support. The engineering challenge is to |
38 smoothly adapt this theory to a theorem prover environment, in our case |
38 smoothly adapt this theory to a theorem prover environment, in our case |
39 Isabelle/HOL. We present a formalisation of this work that is based on a |
39 Isabelle/HOL. For this we have to make the theory compatible with choice |
40 unified atom type and that represents permutations by bijective functions from |
40 principles, which the work by Pitts is not. We present a formalisation of |
41 atoms to atoms. Interestingly, we allow swappings, which are permutations |
41 this work that is based on a unified atom type and that represents |
42 build from two atoms, to be ill-sorted. Furthermore we extend the nominal |
42 permutations by bijective functions from atoms to atoms. Interestingly, we |
43 logic work with names that carry additional information and with a |
43 allow swappings, which are permutations build from two atoms, to be |
44 formalisation of abstractions that bind finite sets of names. |
44 ill-sorted. We extend the nominal logic work with a formalisation of an |
|
45 abstraction operator that binds sets of names. |
45 \end{abstract} |
46 \end{abstract} |
46 |
47 |
47 % generated text of all theories |
48 % generated text of all theories |
48 \input{session} |
49 \input{session} |
49 |
50 |