36 \begin{abstract} |
36 \begin{abstract} |
37 In his nominal logic work, Pitts introduced a beautiful theory about names and |
37 In his nominal logic work, Pitts introduced a beautiful theory about names and |
38 binding based on the notions of atoms, permutations and support. The |
38 binding based on the notions of atoms, permutations and support. The |
39 engineering challenge is to smoothly adapt this theory to a theorem prover |
39 engineering challenge is to smoothly adapt this theory to a theorem prover |
40 environment, in our case Isabelle/HOL. For this we have to formulate the |
40 environment, in our case Isabelle/HOL. For this we have to formulate the |
41 theory so that it is compatible with HOL, which the original formulation by |
41 theory so that it is compatible with Higher-Order Logic, which the original formulation by |
42 Pitts is not. We achieve this by not requiring that every object in our |
42 Pitts is not. We achieve this by not requiring that every construction has |
43 discourse has finite support. We present a formalisation that is based on a |
43 to have finite support. We present a formalisation that is based on a |
44 unified atom type and that represents permutations by bijective functions from |
44 unified atom type and that represents permutations by bijective functions from |
45 atoms to atoms. Interestingly, we allow swappings, which are permutations |
45 atoms to atoms. Interestingly, we allow swappings, which are permutations |
46 build from two atoms, to be ill-sorted. We also describe a formalisation of |
46 build from two atoms, to be ill-sorted. We also describe a formalisation of |
47 two abstraction operators that bind sets of names. |
47 two abstraction operators that bind sets of names. |
48 \end{abstract} |
48 \end{abstract} |