| author | Christian Urban <urbanc@in.tum.de> |
| Fri, 23 Jul 2010 16:42:47 +0200 | |
| changeset 2381 | fd85f4921654 |
| parent 2345 | a908ea36054f |
| child 2488 | 1c18f2cf3923 |
| permissions | -rw-r--r-- |
|
2219
dff64b2e7ec3
adapted to the official sigplan style file (this gives us more space)
Christian Urban <urbanc@in.tum.de>
parents:
2216
diff
changeset
|
1 |
\documentclass{sigplanconf}
|
|
1493
52f68b524fd2
slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents:
1485
diff
changeset
|
2 |
\usepackage{isabelle}
|
|
52f68b524fd2
slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents:
1485
diff
changeset
|
3 |
\usepackage{isabellesym}
|
|
52f68b524fd2
slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents:
1485
diff
changeset
|
4 |
\usepackage{amsmath}
|
|
52f68b524fd2
slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents:
1485
diff
changeset
|
5 |
\usepackage{amssymb}
|
| 1579 | 6 |
\usepackage{amsthm}
|
|
1506
7c607df46a0a
slightly more in the paper
Christian Urban <urbanc@in.tum.de>
parents:
1493
diff
changeset
|
7 |
\usepackage{tikz}
|
|
7c607df46a0a
slightly more in the paper
Christian Urban <urbanc@in.tum.de>
parents:
1493
diff
changeset
|
8 |
\usepackage{pgf}
|
|
7c607df46a0a
slightly more in the paper
Christian Urban <urbanc@in.tum.de>
parents:
1493
diff
changeset
|
9 |
\usepackage{pdfsetup}
|
|
1523
eb95360d6ac6
another little bit for the introduction
Christian Urban <urbanc@in.tum.de>
parents:
1520
diff
changeset
|
10 |
\usepackage{ot1patch}
|
| 1607 | 11 |
\usepackage{times}
|
| 1687 | 12 |
\usepackage{boxedminipage}
|
| 1739 | 13 |
\usepackage{proof}
|
|
1737
8b6a285ad480
polished everything up to TODO
Christian Urban <urbanc@in.tum.de>
parents:
1735
diff
changeset
|
14 |
|
| 1961 | 15 |
\allowdisplaybreaks |
|
754
b85875d65b10
added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
\urlstyle{rm}
|
|
b85875d65b10
added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
\isabellestyle{it}
|
|
1617
99cee15cb5ff
more tuning in the paper
Christian Urban <urbanc@in.tum.de>
parents:
1607
diff
changeset
|
18 |
\renewcommand{\isastyleminor}{\it}%
|
|
99cee15cb5ff
more tuning in the paper
Christian Urban <urbanc@in.tum.de>
parents:
1607
diff
changeset
|
19 |
\renewcommand{\isastyle}{\normalsize\it}%
|
|
754
b85875d65b10
added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
|
|
1523
eb95360d6ac6
another little bit for the introduction
Christian Urban <urbanc@in.tum.de>
parents:
1520
diff
changeset
|
21 |
\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
|
|
eb95360d6ac6
another little bit for the introduction
Christian Urban <urbanc@in.tum.de>
parents:
1520
diff
changeset
|
22 |
\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
|
|
1493
52f68b524fd2
slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents:
1485
diff
changeset
|
23 |
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
|
|
52f68b524fd2
slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents:
1485
diff
changeset
|
24 |
\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}}
|
|
52f68b524fd2
slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents:
1485
diff
changeset
|
25 |
\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
|
|
52f68b524fd2
slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents:
1485
diff
changeset
|
26 |
\renewcommand{\isasymequiv}{$\dn$}
|
| 1687 | 27 |
%%\renewcommand{\isasymiota}{}
|
|
1737
8b6a285ad480
polished everything up to TODO
Christian Urban <urbanc@in.tum.de>
parents:
1735
diff
changeset
|
28 |
\renewcommand{\isasymxi}{$..$}
|
|
1493
52f68b524fd2
slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents:
1485
diff
changeset
|
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
9f55d7927e5b
more on the strong induction section
Christian Urban <urbanc@in.tum.de>
parents:
1754
diff
changeset
|
40 |
\newcommand{\isasymAL}{\makebox[0mm][l]{$^\alpha$}}
|
| 2345 | 41 |
\newcommand{\isasymPRIME}{\makebox[0mm][l]{$'$}}
|
|
1520
6ac75fd979d4
more of the introduction
Christian Urban <urbanc@in.tum.de>
parents:
1517
diff
changeset
|
42 |
\newcommand{\LET}{\;\mathtt{let}\;}
|
|
6ac75fd979d4
more of the introduction
Christian Urban <urbanc@in.tum.de>
parents:
1517
diff
changeset
|
43 |
\newcommand{\IN}{\;\mathtt{in}\;}
|
|
6ac75fd979d4
more of the introduction
Christian Urban <urbanc@in.tum.de>
parents:
1517
diff
changeset
|
44 |
\newcommand{\END}{\;\mathtt{end}\;}
|
|
6ac75fd979d4
more of the introduction
Christian Urban <urbanc@in.tum.de>
parents:
1517
diff
changeset
|
45 |
\newcommand{\AND}{\;\mathtt{and}\;}
|
| 1572 | 46 |
\newcommand{\fv}{\mathit{fv}}
|
|
1493
52f68b524fd2
slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents:
1485
diff
changeset
|
47 |
|
| 1703 | 48 |
\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
|
|
1328
531dcebbf483
start of paper - does not compile yet
Christian Urban <urbanc@in.tum.de>
parents:
754
diff
changeset
|
49 |
%----------------- theorem definitions ---------- |
| 1579 | 50 |
\theoremstyle{plain}
|
51 |
\newtheorem{thm}{Theorem}[section]
|
|
52 |
\newtheorem{property}[thm]{Property}
|
|
53 |
\newtheorem{lemma}[thm]{Lemma}
|
|
54 |
\newtheorem{defn}[thm]{Definition}
|
|
55 |
\newtheorem{exmple}[thm]{Example}
|
|
|
1328
531dcebbf483
start of paper - does not compile yet
Christian Urban <urbanc@in.tum.de>
parents:
754
diff
changeset
|
56 |
|
|
531dcebbf483
start of paper - does not compile yet
Christian Urban <urbanc@in.tum.de>
parents:
754
diff
changeset
|
57 |
%-------------------- environment definitions ----------------- |
|
531dcebbf483
start of paper - does not compile yet
Christian Urban <urbanc@in.tum.de>
parents:
754
diff
changeset
|
58 |
\newenvironment{proof-of}[1]{{\em Proof of #1:}}{}
|
|
754
b85875d65b10
added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
59 |
|
|
1485
c004e7448dca
temporarily disabled tests in Nominal/ROOT
Christian Urban <urbanc@in.tum.de>
parents:
1484
diff
changeset
|
60 |
|
|
754
b85875d65b10
added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
61 |
\begin{document}
|
|
b85875d65b10
added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
62 |
|
|
2216
1a9dbfe04f7d
new title for POPL paper
Christian Urban <urbanc@in.tum.de>
parents:
1961
diff
changeset
|
63 |
\title{\LARGE\bf General Bindings and Alpha-Equivalence in Nominal Isabelle}
|
|
2219
dff64b2e7ec3
adapted to the official sigplan style file (this gives us more space)
Christian Urban <urbanc@in.tum.de>
parents:
2216
diff
changeset
|
64 |
\authorinfo{Christian Urban and Cezary Kaliszyk}
|
|
dff64b2e7ec3
adapted to the official sigplan style file (this gives us more space)
Christian Urban <urbanc@in.tum.de>
parents:
2216
diff
changeset
|
65 |
{TU Munich, Germany}
|
| 2341 | 66 |
{\{urbanc, kaliszyk\}@in.tum.de}
|
|
754
b85875d65b10
added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
67 |
\maketitle |
|
b85875d65b10
added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
68 |
|
|
1328
531dcebbf483
start of paper - does not compile yet
Christian Urban <urbanc@in.tum.de>
parents:
754
diff
changeset
|
69 |
\begin{abstract}
|
| 2341 | 70 |
Nominal Isabelle is a definitional extension of the poular Isabelle/HOL theorem |
|
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>
parents:
1506
diff
changeset
|
71 |
prover. It provides a proving infrastructure for convenient reasoning about |
| 1607 | 72 |
programming language calculi involving named bound variables (as |
|
1528
d6ee4a1b34ce
more tuning on the paper
Christian Urban <urbanc@in.tum.de>
parents:
1524
diff
changeset
|
73 |
opposed to de-Bruijn indices). In this paper we present an extension of |
| 1556 | 74 |
Nominal Isabelle for dealing with general bindings, that means |
| 1657 | 75 |
term-constructors where multiple variables are bound at once. Such general |
76 |
bindings are ubiquitous in programming language research and only very |
|
| 1566 | 77 |
poorly supported with single binders, such as lambda-abstractions. Our |
| 2381 | 78 |
extension includes new definitions of $\alpha$-equivalence and establishes |
| 2341 | 79 |
automatically the reasoning infrastructure for $\alpha$-equated terms. We |
| 1687 | 80 |
also prove strong induction principles that have the usual variable |
| 1566 | 81 |
convention already built in. |
|
1328
531dcebbf483
start of paper - does not compile yet
Christian Urban <urbanc@in.tum.de>
parents:
754
diff
changeset
|
82 |
\end{abstract}
|
|
754
b85875d65b10
added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
83 |
|
| 2342 | 84 |
%\category{F.4.1}{subcategory}{third-level}
|
|
2219
dff64b2e7ec3
adapted to the official sigplan style file (this gives us more space)
Christian Urban <urbanc@in.tum.de>
parents:
2216
diff
changeset
|
85 |
|
|
dff64b2e7ec3
adapted to the official sigplan style file (this gives us more space)
Christian Urban <urbanc@in.tum.de>
parents:
2216
diff
changeset
|
86 |
\terms |
| 2341 | 87 |
formal reasoning, programming language calculi |
|
2219
dff64b2e7ec3
adapted to the official sigplan style file (this gives us more space)
Christian Urban <urbanc@in.tum.de>
parents:
2216
diff
changeset
|
88 |
|
|
dff64b2e7ec3
adapted to the official sigplan style file (this gives us more space)
Christian Urban <urbanc@in.tum.de>
parents:
2216
diff
changeset
|
89 |
\keywords |
| 2341 | 90 |
nominal logic work, variable convention |
|
2219
dff64b2e7ec3
adapted to the official sigplan style file (this gives us more space)
Christian Urban <urbanc@in.tum.de>
parents:
2216
diff
changeset
|
91 |
|
|
1493
52f68b524fd2
slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents:
1485
diff
changeset
|
92 |
|
|
754
b85875d65b10
added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
93 |
\input{session}
|
|
b85875d65b10
added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
94 |
|
|
1493
52f68b524fd2
slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents:
1485
diff
changeset
|
95 |
\bibliographystyle{plain}
|
|
52f68b524fd2
slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents:
1485
diff
changeset
|
96 |
\bibliography{root}
|
|
754
b85875d65b10
added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
97 |
|
|
b85875d65b10
added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
98 |
\end{document}
|
|
b85875d65b10
added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
99 |
|
|
b85875d65b10
added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
100 |
%%% Local Variables: |
|
b85875d65b10
added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
101 |
%%% mode: latex |
|
b85875d65b10
added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
102 |
%%% TeX-master: t |
|
b85875d65b10
added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
103 |
%%% End: |