Paper/document/root.tex
author Christian Urban <urbanc@in.tum.de>
Thu, 01 Apr 2010 15:41:48 +0200
changeset 1754 0ce4f938e8cc
parent 1752 9e09253c80cf
child 1764 9f55d7927e5b
permissions -rw-r--r--
current state
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1485
c004e7448dca temporarily disabled tests in Nominal/ROOT
Christian Urban <urbanc@in.tum.de>
parents: 1484
diff changeset
     1
\documentclass{acmconf}
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
5b0bdd64956e more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 1572
diff changeset
     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
ac69ed8303cc tuned paper
Christian Urban <urbanc@in.tum.de>
parents: 1579
diff changeset
    11
\usepackage{times}
1687
51bc795b81fd more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 1657
diff changeset
    12
\usepackage{boxedminipage}
1739
468c3c1adcba more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 1737
diff changeset
    13
\usepackage{proof}
1737
8b6a285ad480 polished everything up to TODO
Christian Urban <urbanc@in.tum.de>
parents: 1735
diff changeset
    14
754
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
\urlstyle{rm}
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
\isabellestyle{it}
1617
99cee15cb5ff more tuning in the paper
Christian Urban <urbanc@in.tum.de>
parents: 1607
diff changeset
    17
\renewcommand{\isastyleminor}{\it}%
99cee15cb5ff more tuning in the paper
Christian Urban <urbanc@in.tum.de>
parents: 1607
diff changeset
    18
\renewcommand{\isastyle}{\normalsize\it}%
754
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
1523
eb95360d6ac6 another little bit for the introduction
Christian Urban <urbanc@in.tum.de>
parents: 1520
diff changeset
    20
\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
eb95360d6ac6 another little bit for the introduction
Christian Urban <urbanc@in.tum.de>
parents: 1520
diff changeset
    21
\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
1493
52f68b524fd2 slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents: 1485
diff changeset
    22
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
52f68b524fd2 slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents: 1485
diff changeset
    23
\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}}
52f68b524fd2 slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents: 1485
diff changeset
    24
\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
52f68b524fd2 slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents: 1485
diff changeset
    25
\renewcommand{\isasymequiv}{$\dn$}
1687
51bc795b81fd more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 1657
diff changeset
    26
%%\renewcommand{\isasymiota}{}
1737
8b6a285ad480 polished everything up to TODO
Christian Urban <urbanc@in.tum.de>
parents: 1735
diff changeset
    27
\renewcommand{\isasymxi}{$..$}
1493
52f68b524fd2 slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents: 1485
diff changeset
    28
\renewcommand{\isasymemptyset}{$\varnothing$}
1657
Christian Urban <urbanc@in.tum.de>
parents: 1617
diff changeset
    29
\newcommand{\isasymnotapprox}{$\not\approx$}
Christian Urban <urbanc@in.tum.de>
parents: 1617
diff changeset
    30
\newcommand{\isasymLET}{$\mathtt{let}$}
Christian Urban <urbanc@in.tum.de>
parents: 1617
diff changeset
    31
\newcommand{\isasymAND}{$\mathtt{and}$}
Christian Urban <urbanc@in.tum.de>
parents: 1617
diff changeset
    32
\newcommand{\isasymIN}{$\mathtt{in}$}
Christian Urban <urbanc@in.tum.de>
parents: 1617
diff changeset
    33
\newcommand{\isasymEND}{$\mathtt{end}$}
Christian Urban <urbanc@in.tum.de>
parents: 1617
diff changeset
    34
\newcommand{\isasymBIND}{$\mathtt{bind}$}
Christian Urban <urbanc@in.tum.de>
parents: 1617
diff changeset
    35
\newcommand{\isasymANIL}{$\mathtt{anil}$}
Christian Urban <urbanc@in.tum.de>
parents: 1617
diff changeset
    36
\newcommand{\isasymACONS}{$\mathtt{acons}$}
1687
51bc795b81fd more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 1657
diff changeset
    37
\newcommand{\isasymCASE}{$\mathtt{case}$}
51bc795b81fd more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 1657
diff changeset
    38
\newcommand{\isasymOF}{$\mathtt{of}$}
1520
6ac75fd979d4 more of the introduction
Christian Urban <urbanc@in.tum.de>
parents: 1517
diff changeset
    39
\newcommand{\LET}{\;\mathtt{let}\;}
6ac75fd979d4 more of the introduction
Christian Urban <urbanc@in.tum.de>
parents: 1517
diff changeset
    40
\newcommand{\IN}{\;\mathtt{in}\;}
6ac75fd979d4 more of the introduction
Christian Urban <urbanc@in.tum.de>
parents: 1517
diff changeset
    41
\newcommand{\END}{\;\mathtt{end}\;}
6ac75fd979d4 more of the introduction
Christian Urban <urbanc@in.tum.de>
parents: 1517
diff changeset
    42
\newcommand{\AND}{\;\mathtt{and}\;}
1572
0368aef38e6a more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 1566
diff changeset
    43
\newcommand{\fv}{\mathit{fv}}
1493
52f68b524fd2 slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents: 1485
diff changeset
    44
1703
ac2d0d4ea497 more of the paper
Christian Urban <urbanc@in.tum.de>
parents: 1687
diff changeset
    45
\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
    46
%----------------- theorem definitions ----------
1579
5b0bdd64956e more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 1572
diff changeset
    47
\theoremstyle{plain}
5b0bdd64956e more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 1572
diff changeset
    48
\newtheorem{thm}{Theorem}[section]
5b0bdd64956e more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 1572
diff changeset
    49
\newtheorem{property}[thm]{Property}
5b0bdd64956e more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 1572
diff changeset
    50
\newtheorem{lemma}[thm]{Lemma}
5b0bdd64956e more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 1572
diff changeset
    51
\newtheorem{defn}[thm]{Definition}
5b0bdd64956e more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 1572
diff changeset
    52
\newtheorem{exmple}[thm]{Example}
1328
531dcebbf483 start of paper - does not compile yet
Christian Urban <urbanc@in.tum.de>
parents: 754
diff changeset
    53
531dcebbf483 start of paper - does not compile yet
Christian Urban <urbanc@in.tum.de>
parents: 754
diff changeset
    54
%-------------------- environment definitions -----------------
531dcebbf483 start of paper - does not compile yet
Christian Urban <urbanc@in.tum.de>
parents: 754
diff changeset
    55
\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
    56
1485
c004e7448dca temporarily disabled tests in Nominal/ROOT
Christian Urban <urbanc@in.tum.de>
parents: 1484
diff changeset
    57
754
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    58
\begin{document}
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    59
1545
f32981105089 more one the paper
Christian Urban <urbanc@in.tum.de>
parents: 1535
diff changeset
    60
\title{\LARGE\bf General Bindings in Nominal Isabelle,\\ or How to
1328
531dcebbf483 start of paper - does not compile yet
Christian Urban <urbanc@in.tum.de>
parents: 754
diff changeset
    61
  Formalise Core-Haskell}
1752
9e09253c80cf added alpha_bn definition
Christian Urban <urbanc@in.tum.de>
parents: 1739
diff changeset
    62
\author{Christian Urban, Cezary Kaliszyk}
9e09253c80cf added alpha_bn definition
Christian Urban <urbanc@in.tum.de>
parents: 1739
diff changeset
    63
\affiliation{TU Munich, Germany}
754
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    64
\maketitle
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    65
1328
531dcebbf483 start of paper - does not compile yet
Christian Urban <urbanc@in.tum.de>
parents: 754
diff changeset
    66
\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>
parents: 1506
diff changeset
    67
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>
parents: 1506
diff changeset
    68
prover. It provides a proving infrastructure for convenient reasoning about
1607
ac69ed8303cc tuned paper
Christian Urban <urbanc@in.tum.de>
parents: 1579
diff changeset
    69
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
    70
opposed to de-Bruijn indices). In this paper we present an extension of
1556
a7072d498723 more work on the paper
Christian Urban <urbanc@in.tum.de>
parents: 1550
diff changeset
    71
Nominal Isabelle for dealing with general bindings, that means
1657
Christian Urban <urbanc@in.tum.de>
parents: 1617
diff changeset
    72
term-constructors where multiple variables are bound at once. Such general
Christian Urban <urbanc@in.tum.de>
parents: 1617
diff changeset
    73
bindings are ubiquitous in programming language research and only very
1566
2facd6645599 tuned paper
Christian Urban <urbanc@in.tum.de>
parents: 1556
diff changeset
    74
poorly supported with single binders, such as lambda-abstractions. Our
2facd6645599 tuned paper
Christian Urban <urbanc@in.tum.de>
parents: 1556
diff changeset
    75
extension includes novel definitions of alpha-equivalence and establishes
2facd6645599 tuned paper
Christian Urban <urbanc@in.tum.de>
parents: 1556
diff changeset
    76
automatically the reasoning infrastructure for alpha-equated terms. We
1687
51bc795b81fd more on the paper
Christian Urban <urbanc@in.tum.de>
parents: 1657
diff changeset
    77
also prove strong induction principles that have the usual variable
1566
2facd6645599 tuned paper
Christian Urban <urbanc@in.tum.de>
parents: 1556
diff changeset
    78
convention already built in.
1328
531dcebbf483 start of paper - does not compile yet
Christian Urban <urbanc@in.tum.de>
parents: 754
diff changeset
    79
\end{abstract}
754
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    80
1493
52f68b524fd2 slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents: 1485
diff changeset
    81
754
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    82
\input{session}
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    83
1493
52f68b524fd2 slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents: 1485
diff changeset
    84
\bibliographystyle{plain}
52f68b524fd2 slightly more of the paper
Christian Urban <urbanc@in.tum.de>
parents: 1485
diff changeset
    85
\bibliography{root}
754
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    86
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    87
\end{document}
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    88
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    89
%%% Local Variables:
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    90
%%% mode: latex
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    91
%%% TeX-master: t
b85875d65b10 added a paper for possible notes
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    92
%%% End: