37 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{} |
37 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{} |
38 |
38 |
39 |
39 |
40 \begin{document} |
40 \begin{document} |
41 |
41 |
42 \title{\LARGE\bf General Binding Structures in Nominal Isabelle,\\ or How to |
42 \title{\LARGE\bf General Bindings in Nominal Isabelle,\\ or How to |
43 Formalise Core-Haskell} |
43 Formalise Core-Haskell} |
44 \maketitle |
44 \maketitle |
45 |
45 |
46 \maketitle |
46 \maketitle |
47 \begin{abstract} |
47 \begin{abstract} |
48 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
48 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
49 prover. It provides a proving infrastructure for convenient reasoning about |
49 prover. It provides a proving infrastructure for convenient reasoning about |
50 programming language calculi involving bound variables that have names (as |
50 programming language calculi involving bound variables that have names (as |
51 opposed to de-Bruijn indices). In this paper we present an extension of |
51 opposed to de-Bruijn indices). In this paper we present an extension of |
52 Nominal Isabelle in order to deal with general binding structures. Such |
52 Nominal Isabelle for dealing with general binding structures, that means |
|
53 where multiple variables are bound at once. Such |
53 binding structures are ubiquitous in programming language research and only |
54 binding structures are ubiquitous in programming language research and only |
54 very poorly supported with single binders, such as the lambdas in the |
55 very poorly supported with single binders, such as the lambdas in the |
55 lambda-calculus. For our extension we introduce novel definitions of |
56 lambda-calculus. Our extension includes novel definitions of |
56 alpha-equivalence and establish automatically the reasoning infrastructure for |
57 alpha-equivalence and establishes automatically the reasoning infrastructure for |
57 alpha-equated terms. This includes strong induction principles that have the |
58 alpha-equated terms. This includes strong induction principles that have the |
58 variable convention already built in. |
59 usual variable convention already built in. |
59 \end{abstract} |
60 \end{abstract} |
60 |
61 |
61 |
62 |
62 \input{session} |
63 \input{session} |
63 |
64 |