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. For this we have to make the theory compatible with choice |
39 Isabelle/HOL. For this we have to formulate the theory so that it is |
40 principles, which the work by Pitts is not. We present a formalisation of |
40 compatible with choice principles, which the work by Pitts is not. We |
41 this work that is based on a unified atom type and that represents |
41 present a formalisation of this work that is based on a unified atom type |
42 permutations by bijective functions from atoms to atoms. Interestingly, we |
42 and that represents permutations by bijective functions from atoms to atoms. |
43 allow swappings, which are permutations build from two atoms, to be |
43 Interestingly, we allow swappings, which are permutations build from two |
44 ill-sorted. We extend the nominal logic work with a formalisation of an |
44 atoms, to be ill-sorted. We also describe a formalisation of an |
45 abstraction operator that binds sets of names. |
45 abstraction operator that binds sets of names. |
46 \end{abstract} |
46 \end{abstract} |
47 |
47 |
48 % generated text of all theories |
48 % generated text of all theories |
49 \input{session} |
49 \input{session} |