equal
deleted
inserted
replaced
66 \begin{document} |
66 \begin{document} |
67 |
67 |
68 \title[Genral Bindings]{General Bindings and Alpha-Equivalence in Nominal |
68 \title[Genral Bindings]{General Bindings and Alpha-Equivalence in Nominal |
69 Isabelle$^\star$} |
69 Isabelle$^\star$} |
70 \author{Christian Urban} |
70 \author{Christian Urban} |
71 \address{Technical University of Munich, Germany} |
71 \address{King's College London, United Kingdom} |
72 \email{urbanc@in.tum.de} |
72 \email{christian.urban@kcl.ac.uk} |
73 |
73 |
74 \author{Cezary Kaliszyk} |
74 \author{Cezary Kaliszyk} |
75 \address{University of Tsukuba, Japan} |
75 \address{University of Tsukuba, Japan} |
76 \email{kaliszyk@cs.tsukuba.ac.jp} |
76 \email{kaliszyk@cs.tsukuba.ac.jp} |
77 \thanks{$^\star$~This is a revised and expanded version of~\cite{UrbanKaliszyk11}} |
77 \thanks{$^\star$~This is a revised and expanded version of~\cite{UrbanKaliszyk11}} |
83 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
83 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
84 prover. It provides a proving infrastructure for reasoning about |
84 prover. It provides a proving infrastructure for reasoning about |
85 programming language calculi involving named bound variables (as |
85 programming language calculi involving named bound variables (as |
86 opposed to de-Bruijn indices). In this paper we present an extension of |
86 opposed to de-Bruijn indices). In this paper we present an extension of |
87 Nominal Isabelle for dealing with general bindings, that means |
87 Nominal Isabelle for dealing with general bindings, that means |
88 term-constructors where multiple variables are bound at once. Such general |
88 term constructors where multiple variables are bound at once. Such general |
89 bindings are ubiquitous in programming language research and only very |
89 bindings are ubiquitous in programming language research and only very |
90 poorly supported with single binders, such as lambda-abstractions. Our |
90 poorly supported with single binders, such as lambda-abstractions. Our |
91 extension includes new definitions of alpha-equivalence and establishes |
91 extension includes new definitions of alpha-equivalence and establishes |
92 automatically the reasoning infrastructure for alpha-equated terms. We |
92 automatically the reasoning infrastructure for alpha-equated terms. We |
93 also prove strong induction principles that have the usual variable |
93 also prove strong induction principles that have the usual variable |