equal
deleted
inserted
replaced
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. In this paper we present an extension of Nominal |
50 programming language calculi involving bound variables that have names (as |
51 Isabelle in order to deal with general binding structures. Such binding structures |
51 opposed to de-Bruijn indices). In this paper we present an extension of |
52 are ubiquitous in programming language research and only very poorly supported |
52 Nominal Isabelle in order to deal with general binding structures. Such |
53 with single binders, as for example found in the lambda-calculus. For our |
53 binding structures are ubiquitous in programming language research and only |
54 extension we introduce novel definitions of alpha-equivalence and establish |
54 very poorly supported with single binders, as for example found in the |
55 automatically the reasoning infrastructure for alpha-equated terms. This |
55 lambda-calculus. For our extension we introduce novel definitions of |
56 includes a strong induction principle which has the variable convention |
56 alpha-equivalence and establish automatically the reasoning infrastructure for |
57 already built in. |
57 alpha-equated terms. This includes strong induction principles that have the |
|
58 variable convention already built in. |
58 \end{abstract} |
59 \end{abstract} |
59 |
60 |
60 |
61 |
61 \input{session} |
62 \input{session} |
62 |
63 |