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:
|