equal
deleted
inserted
replaced
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 for dealing with general binding structures, that means |
52 Nominal Isabelle for dealing with general bindings, that means |
53 where multiple variables are bound at once. Such |
53 term-constructors where multiple variables are bound at once. Such |
54 binding structures are ubiquitous in programming language research and only |
54 binding structures are ubiquitous in programming language research and only |
55 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 |
56 lambda-calculus. Our extension includes novel definitions of |
56 lambda-calculus. Our extension includes novel definitions of |
57 alpha-equivalence and establishes automatically the reasoning infrastructure for |
57 alpha-equivalence and establishes automatically the reasoning infrastructure for |
58 alpha-equated terms. We can also provide strong induction principles that have |
58 alpha-equated terms. We can also provide strong induction principles that have |