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 formulate the theory so that it is |
39 Isabelle/HOL. For this we have to formulate the theory so that it is |
40 compatible with choice principles, which the work by Pitts is not. We |
40 compatible with HOL, which the original formulation by Pitts is not. We |
41 present a formalisation of this work that is based on a unified atom type |
41 present a formalisation that is based on a unified atom type |
42 and that represents permutations by bijective functions from atoms to atoms. |
42 and that represents permutations by bijective functions from atoms to atoms. |
43 Interestingly, we allow swappings, which are permutations build from two |
43 Interestingly, we allow swappings, which are permutations build from two |
44 atoms, to be ill-sorted. We also describe a formalisation of an |
44 atoms, to be ill-sorted. We also describe a formalisation of two |
45 abstraction operator that binds sets of names. |
45 abstraction operators that bind 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} |
50 |
50 |