1485
+ − 1 \documentclass{acmconf}
1493
+ − 2 \usepackage{isabelle}
+ − 3 \usepackage{isabellesym}
+ − 4 \usepackage{amsmath}
+ − 5 \usepackage{amssymb}
1579
+ − 6 \usepackage{amsthm}
1506
+ − 7 \usepackage{tikz}
+ − 8 \usepackage{pgf}
+ − 9 \usepackage{pdfsetup}
1523
+ − 10 \usepackage{ot1patch}
1607
+ − 11 \usepackage{times}
1687
+ − 12 \usepackage{boxedminipage}
1739
+ − 13 \usepackage{proof}
1737
+ − 14
1961
+ − 15 \allowdisplaybreaks
754
+ − 16 \urlstyle{rm}
+ − 17 \isabellestyle{it}
1617
+ − 18 \renewcommand{\isastyleminor}{\it}%
+ − 19 \renewcommand{\isastyle}{\normalsize\it}%
754
+ − 20
1523
+ − 21 \DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
+ − 22 \DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
1493
+ − 23 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+ − 24 \renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}}
+ − 25 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+ − 26 \renewcommand{\isasymequiv}{$\dn$}
1687
+ − 27 %%\renewcommand{\isasymiota}{}
1737
+ − 28 \renewcommand{\isasymxi}{$..$}
1493
+ − 29 \renewcommand{\isasymemptyset}{$\varnothing$}
1657
+ − 30 \newcommand{\isasymnotapprox}{$\not\approx$}
+ − 31 \newcommand{\isasymLET}{$\mathtt{let}$}
+ − 32 \newcommand{\isasymAND}{$\mathtt{and}$}
+ − 33 \newcommand{\isasymIN}{$\mathtt{in}$}
+ − 34 \newcommand{\isasymEND}{$\mathtt{end}$}
+ − 35 \newcommand{\isasymBIND}{$\mathtt{bind}$}
+ − 36 \newcommand{\isasymANIL}{$\mathtt{anil}$}
+ − 37 \newcommand{\isasymACONS}{$\mathtt{acons}$}
1687
+ − 38 \newcommand{\isasymCASE}{$\mathtt{case}$}
+ − 39 \newcommand{\isasymOF}{$\mathtt{of}$}
1764
+ − 40 \newcommand{\isasymAL}{\makebox[0mm][l]{$^\alpha$}}
1520
+ − 41 \newcommand{\LET}{\;\mathtt{let}\;}
+ − 42 \newcommand{\IN}{\;\mathtt{in}\;}
+ − 43 \newcommand{\END}{\;\mathtt{end}\;}
+ − 44 \newcommand{\AND}{\;\mathtt{and}\;}
1572
+ − 45 \newcommand{\fv}{\mathit{fv}}
1493
+ − 46
1703
+ − 47 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
1328
+ − 48 %----------------- theorem definitions ----------
1579
+ − 49 \theoremstyle{plain}
+ − 50 \newtheorem{thm}{Theorem}[section]
+ − 51 \newtheorem{property}[thm]{Property}
+ − 52 \newtheorem{lemma}[thm]{Lemma}
+ − 53 \newtheorem{defn}[thm]{Definition}
+ − 54 \newtheorem{exmple}[thm]{Example}
1328
+ − 55
+ − 56 %-------------------- environment definitions -----------------
+ − 57 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{}
754
+ − 58
1485
+ − 59
754
+ − 60 \begin{document}
+ − 61
1545
+ − 62 \title{\LARGE\bf General Bindings in Nominal Isabelle,\\ or How to
1328
+ − 63 Formalise Core-Haskell}
1752
+ − 64 \author{Christian Urban, Cezary Kaliszyk}
+ − 65 \affiliation{TU Munich, Germany}
754
+ − 66 \maketitle
+ − 67
1328
+ − 68 \begin{abstract}
1517
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 69 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
62d6f7acc110
corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 70 prover. It provides a proving infrastructure for convenient reasoning about
1607
+ − 71 programming language calculi involving named bound variables (as
1528
+ − 72 opposed to de-Bruijn indices). In this paper we present an extension of
1556
+ − 73 Nominal Isabelle for dealing with general bindings, that means
1657
+ − 74 term-constructors where multiple variables are bound at once. Such general
+ − 75 bindings are ubiquitous in programming language research and only very
1566
+ − 76 poorly supported with single binders, such as lambda-abstractions. Our
+ − 77 extension includes novel definitions of alpha-equivalence and establishes
+ − 78 automatically the reasoning infrastructure for alpha-equated terms. We
1687
+ − 79 also prove strong induction principles that have the usual variable
1566
+ − 80 convention already built in.
1328
+ − 81 \end{abstract}
754
+ − 82
1493
+ − 83
754
+ − 84 \input{session}
+ − 85
1493
+ − 86 \bibliographystyle{plain}
+ − 87 \bibliography{root}
754
+ − 88
+ − 89 \end{document}
+ − 90
+ − 91 %%% Local Variables:
+ − 92 %%% mode: latex
+ − 93 %%% TeX-master: t
+ − 94 %%% End: