29 \institute{Portland State University \and Technical University of Munich} |
29 \institute{Portland State University \and Technical University of Munich} |
30 \maketitle |
30 \maketitle |
31 |
31 |
32 \begin{abstract} |
32 \begin{abstract} |
33 Pitts et al introduced a beautiful theory about names and binding based on the |
33 Pitts et al introduced a beautiful theory about names and binding based on the |
34 notions of atoms, permutations and support. The engineering challenge |
34 notions of atoms, permutations and support. The engineering challenge is to |
35 is to smoothly adapt this theory to a theorem prover environment, in our case |
35 smoothly adapt this theory to a theorem prover environment, in our case |
36 Isabelle/HOL. We present a formalisation of this work that is based on a |
36 Isabelle/HOL. We present a formalisation of this work that is based on a |
37 unified atom type (that includes all sorts of atoms) and that represents |
37 unified atom type and that represents permutations by bijective functions from |
38 permutations by bijective functions from atoms to atoms. Interestingly, we |
38 atoms to atoms. Interestingly, we allow swappings, which are permutations |
39 allow swappings, which are permutations build from two atoms, to be |
39 build from two atoms, to be ill-sorted. Furthermore we extend the nominal |
40 ill-sorted. Furthermore we can extend the nominal logic with names that carry |
40 logic work with names that carry additional information. |
41 additional information. |
|
42 \end{abstract} |
41 \end{abstract} |
43 |
42 |
44 % generated text of all theories |
43 % generated text of all theories |
45 \input{session} |
44 \input{session} |
46 |
45 |