equal
deleted
inserted
replaced
73 opposed to de-Bruijn indices). In this paper we present an extension of |
73 opposed to de-Bruijn indices). In this paper we present an extension of |
74 Nominal Isabelle for dealing with general bindings, that means |
74 Nominal Isabelle for dealing with general bindings, that means |
75 term-constructors where multiple variables are bound at once. Such general |
75 term-constructors where multiple variables are bound at once. Such general |
76 bindings are ubiquitous in programming language research and only very |
76 bindings are ubiquitous in programming language research and only very |
77 poorly supported with single binders, such as lambda-abstractions. Our |
77 poorly supported with single binders, such as lambda-abstractions. Our |
78 extension includes novel definitions of $\alpha$-equivalence and establishes |
78 extension includes new definitions of $\alpha$-equivalence and establishes |
79 automatically the reasoning infrastructure for $\alpha$-equated terms. We |
79 automatically the reasoning infrastructure for $\alpha$-equated terms. We |
80 also prove strong induction principles that have the usual variable |
80 also prove strong induction principles that have the usual variable |
81 convention already built in. |
81 convention already built in. |
82 \end{abstract} |
82 \end{abstract} |
83 |
83 |