60 \begin{document} |
60 \begin{document} |
61 |
61 |
62 \title{\LARGE\bf General Bindings and Alpha-Equivalence in Nominal Isabelle} |
62 \title{\LARGE\bf General Bindings and Alpha-Equivalence in Nominal Isabelle} |
63 \authorinfo{Christian Urban and Cezary Kaliszyk} |
63 \authorinfo{Christian Urban and Cezary Kaliszyk} |
64 {TU Munich, Germany} |
64 {TU Munich, Germany} |
65 {urbanc/kaliszyk@in.tum.de} |
65 {\{urbanc, kaliszyk\}@in.tum.de} |
66 \maketitle |
66 \maketitle |
67 |
67 |
68 \begin{abstract} |
68 \begin{abstract} |
69 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
69 Nominal Isabelle is a definitional extension of the poular Isabelle/HOL theorem |
70 prover. It provides a proving infrastructure for convenient reasoning about |
70 prover. It provides a proving infrastructure for convenient reasoning about |
71 programming language calculi involving named bound variables (as |
71 programming language calculi involving named bound variables (as |
72 opposed to de-Bruijn indices). In this paper we present an extension of |
72 opposed to de-Bruijn indices). In this paper we present an extension of |
73 Nominal Isabelle for dealing with general bindings, that means |
73 Nominal Isabelle for dealing with general bindings, that means |
74 term-constructors where multiple variables are bound at once. Such general |
74 term-constructors where multiple variables are bound at once. Such general |
75 bindings are ubiquitous in programming language research and only very |
75 bindings are ubiquitous in programming language research and only very |
76 poorly supported with single binders, such as lambda-abstractions. Our |
76 poorly supported with single binders, such as lambda-abstractions. Our |
77 extension includes novel definitions of alpha-equivalence and establishes |
77 extension includes novel definitions of $\alpha$-equivalence and establishes |
78 automatically the reasoning infrastructure for alpha-equated terms. We |
78 automatically the reasoning infrastructure for $\alpha$-equated terms. We |
79 also prove strong induction principles that have the usual variable |
79 also prove strong induction principles that have the usual variable |
80 convention already built in. |
80 convention already built in. |
81 \end{abstract} |
81 \end{abstract} |
82 |
82 |
83 \category{CR-number}{subcategory}{third-level} |
83 \category{CR-number}{subcategory}{third-level} |
84 |
84 |
85 \terms |
85 \terms |
86 term1, term2 |
86 formal reasoning, programming language calculi |
87 |
87 |
88 \keywords |
88 \keywords |
89 keyword1, keyword2 |
89 nominal logic work, variable convention |
90 |
90 |
91 |
91 |
92 \input{session} |
92 \input{session} |
93 |
93 |
94 \bibliographystyle{plain} |
94 \bibliographystyle{plain} |