54 %%\spnewtheorem{thm}[section]{Theorem} |
54 %%\spnewtheorem{thm}[section]{Theorem} |
55 %%\newtheorem{property}[thm]{Property} |
55 %%\newtheorem{property}[thm]{Property} |
56 %%\newtheorem{lemma}[thm]{Lemma} |
56 %%\newtheorem{lemma}[thm]{Lemma} |
57 %%\spnewtheorem{defn}[theorem]{Definition} |
57 %%\spnewtheorem{defn}[theorem]{Definition} |
58 %%\spnewtheorem{exmple}[theorem]{Example} |
58 %%\spnewtheorem{exmple}[theorem]{Example} |
59 \spnewtheorem{myproperty}{Property}{\bfseries}{\rmfamily} |
59 %%\spnewtheorem{myproperty}{Property}{\bfseries}{\rmfamily} |
60 %-------------------- environment definitions ----------------- |
60 %-------------------- environment definitions ----------------- |
61 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{} |
61 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{} |
62 |
62 |
63 %\addtolength{\textwidth}{2mm} |
63 %\addtolength{\textwidth}{2mm} |
64 \addtolength{\parskip}{-0.33mm} |
64 \addtolength{\parskip}{-0.33mm} |
65 \begin{document} |
65 \begin{document} |
66 |
66 |
67 \title{General Bindings and Alpha-Equivalence\\ in Nominal Isabelle} |
67 \title[Genral Bindings]{General Bindings and Alpha-Equivalence in Nominal Isabelle} |
68 \author{Christian Urban and Cezary Kaliszyk} |
68 \author{Christian Urban} |
69 \institute{TU Munich, Germany} |
69 \address{Technical University of Munich, Germany} |
70 %%%{\{urbanc, kaliszyk\}@in.tum.de} |
70 \email{urbanc@in.tum.de} |
71 \maketitle |
71 |
|
72 \author{Cezary Kaliszyk} |
|
73 \address{University of Tsukuba, Japan} |
|
74 \email{kaliszyk@score.cs.tsukuba.ac.jp} |
|
75 |
|
76 \keywords{Nominal Isabelle, variable convention, formal reasoning} |
|
77 \subjclass{MANDATORY list of acm classifications} |
72 |
78 |
73 \begin{abstract} |
79 \begin{abstract} |
74 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
80 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem |
75 prover. It provides a proving infrastructure for reasoning about |
81 prover. It provides a proving infrastructure for reasoning about |
76 programming language calculi involving named bound variables (as |
82 programming language calculi involving named bound variables (as |
77 opposed to de-Bruijn indices). In this paper we present an extension of |
83 opposed to de-Bruijn indices). In this paper we present an extension of |
78 Nominal Isabelle for dealing with general bindings, that means |
84 Nominal Isabelle for dealing with general bindings, that means |
79 term-constructors where multiple variables are bound at once. Such general |
85 term-constructors where multiple variables are bound at once. Such general |
80 bindings are ubiquitous in programming language research and only very |
86 bindings are ubiquitous in programming language research and only very |
81 poorly supported with single binders, such as lambda-abstractions. Our |
87 poorly supported with single binders, such as lambda-abstractions. Our |
82 extension includes new definitions of $\alpha$-equivalence and establishes |
88 extension includes new definitions of alpha-equivalence and establishes |
83 automatically the reasoning infrastructure for $\alpha$-equated terms. We |
89 automatically the reasoning infrastructure for alpha-equated terms. We |
84 also prove strong induction principles that have the usual variable |
90 also prove strong induction principles that have the usual variable |
85 convention already built in. |
91 convention already built in. |
86 \end{abstract} |
92 \end{abstract} |
87 |
93 |
88 %\category{F.4.1}{subcategory}{third-level} |
94 \maketitle |
89 |
|
90 %\terms |
|
91 %formal reasoning, programming language calculi |
|
92 |
|
93 %\keywords |
|
94 %nominal logic work, variable convention |
|
95 |
|
96 |
|
97 \input{session} |
95 \input{session} |
98 |
96 |
99 \begin{spacing}{0.9} |
97 \bibliographystyle{plain} |
100 \bibliographystyle{plain} |
98 \bibliography{root} |
101 \bibliography{root} |
99 |
102 \end{spacing} |
|
103 |
100 |
104 %\pagebreak |
101 %\pagebreak |
105 %\input{Appendix} |
102 %\input{Appendix} |
106 |
103 |
107 \end{document} |
104 \end{document} |