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