nominal2: Paper/document/root.tex@1f38489f1cf0 (annotated)

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
1961 774d631726ad merged Christian Urban <urbanc@in.tum.de> parents: 1764 diff changeset	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 51bc795b81fd more on the paper Christian Urban <urbanc@in.tum.de> parents: 1657 diff changeset	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 d7dc35222afc merged Christian Urban <urbanc@in.tum.de> parents: 1617 diff changeset	30	\newcommand{\isasymnotapprox}{$\not\approx$}
d7dc35222afc merged Christian Urban <urbanc@in.tum.de> parents: 1617 diff changeset	31	\newcommand{\isasymLET}{$\mathtt{let}$}
d7dc35222afc merged Christian Urban <urbanc@in.tum.de> parents: 1617 diff changeset	32	\newcommand{\isasymAND}{$\mathtt{and}$}
d7dc35222afc merged Christian Urban <urbanc@in.tum.de> parents: 1617 diff changeset	33	\newcommand{\isasymIN}{$\mathtt{in}$}
d7dc35222afc merged Christian Urban <urbanc@in.tum.de> parents: 1617 diff changeset	34	\newcommand{\isasymEND}{$\mathtt{end}$}
d7dc35222afc merged Christian Urban <urbanc@in.tum.de> parents: 1617 diff changeset	35	\newcommand{\isasymBIND}{$\mathtt{bind}$}
d7dc35222afc merged Christian Urban <urbanc@in.tum.de> parents: 1617 diff changeset	36	\newcommand{\isasymANIL}{$\mathtt{anil}$}
d7dc35222afc merged Christian Urban <urbanc@in.tum.de> parents: 1617 diff changeset	37	\newcommand{\isasymACONS}{$\mathtt{acons}$}
1687 51bc795b81fd more on the paper Christian Urban <urbanc@in.tum.de> parents: 1657 diff changeset	38	\newcommand{\isasymCASE}{$\mathtt{case}$}
51bc795b81fd more on the paper Christian Urban <urbanc@in.tum.de> parents: 1657 diff changeset	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$}}
1520 6ac75fd979d4 more of the introduction Christian Urban <urbanc@in.tum.de> parents: 1517 diff changeset	41	\newcommand{\LET}{\;\mathtt{let}\;}
6ac75fd979d4 more of the introduction Christian Urban <urbanc@in.tum.de> parents: 1517 diff changeset	42	\newcommand{\IN}{\;\mathtt{in}\;}
6ac75fd979d4 more of the introduction Christian Urban <urbanc@in.tum.de> parents: 1517 diff changeset	43	\newcommand{\END}{\;\mathtt{end}\;}
6ac75fd979d4 more of the introduction Christian Urban <urbanc@in.tum.de> parents: 1517 diff changeset	44	\newcommand{\AND}{\;\mathtt{and}\;}
1572 0368aef38e6a more on the paper Christian Urban <urbanc@in.tum.de> parents: 1566 diff changeset	45	\newcommand{\fv}{\mathit{fv}}
1493 52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	46
1703 ac2d0d4ea497 more of the paper Christian Urban <urbanc@in.tum.de> parents: 1687 diff changeset	47	\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	48	%----------------- theorem definitions ----------
1579 5b0bdd64956e more on the paper Christian Urban <urbanc@in.tum.de> parents: 1572 diff changeset	49	\theoremstyle{plain}
5b0bdd64956e more on the paper Christian Urban <urbanc@in.tum.de> parents: 1572 diff changeset	50	\newtheorem{thm}{Theorem}[section]
5b0bdd64956e more on the paper Christian Urban <urbanc@in.tum.de> parents: 1572 diff changeset	51	\newtheorem{property}[thm]{Property}
5b0bdd64956e more on the paper Christian Urban <urbanc@in.tum.de> parents: 1572 diff changeset	52	\newtheorem{lemma}[thm]{Lemma}
5b0bdd64956e more on the paper Christian Urban <urbanc@in.tum.de> parents: 1572 diff changeset	53	\newtheorem{defn}[thm]{Definition}
5b0bdd64956e more on the paper Christian Urban <urbanc@in.tum.de> parents: 1572 diff changeset	54	\newtheorem{exmple}[thm]{Example}
1328 531dcebbf483 start of paper - does not compile yet Christian Urban <urbanc@in.tum.de> parents: 754 diff changeset	55
531dcebbf483 start of paper - does not compile yet Christian Urban <urbanc@in.tum.de> parents: 754 diff changeset	56	%-------------------- environment definitions -----------------
531dcebbf483 start of paper - does not compile yet Christian Urban <urbanc@in.tum.de> parents: 754 diff changeset	57	\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	58
1485 c004e7448dca temporarily disabled tests in Nominal/ROOT Christian Urban <urbanc@in.tum.de> parents: 1484 diff changeset	59
754 b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	60	\begin{document}
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	61
1545 f32981105089 more one the paper Christian Urban <urbanc@in.tum.de> parents: 1535 diff changeset	62	\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	63	Formalise Core-Haskell}
1752 9e09253c80cf added alpha_bn definition Christian Urban <urbanc@in.tum.de> parents: 1739 diff changeset	64	\author{Christian Urban, Cezary Kaliszyk}
9e09253c80cf added alpha_bn definition Christian Urban <urbanc@in.tum.de> parents: 1739 diff changeset	65	\affiliation{TU Munich, Germany}
754 b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	66	\maketitle
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	67
1328 531dcebbf483 start of paper - does not compile yet Christian Urban <urbanc@in.tum.de> parents: 754 diff changeset	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> parents: 1506 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> parents: 1506 diff changeset	70	prover. It provides a proving infrastructure for convenient reasoning about
1607 ac69ed8303cc tuned paper Christian Urban <urbanc@in.tum.de> parents: 1579 diff changeset	71	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	72	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	73	Nominal Isabelle for dealing with general bindings, that means
1657 d7dc35222afc merged Christian Urban <urbanc@in.tum.de> parents: 1617 diff changeset	74	term-constructors where multiple variables are bound at once. Such general
d7dc35222afc merged Christian Urban <urbanc@in.tum.de> parents: 1617 diff changeset	75	bindings are ubiquitous in programming language research and only very
1566 2facd6645599 tuned paper Christian Urban <urbanc@in.tum.de> parents: 1556 diff changeset	76	poorly supported with single binders, such as lambda-abstractions. Our
2facd6645599 tuned paper Christian Urban <urbanc@in.tum.de> parents: 1556 diff changeset	77	extension includes novel definitions of alpha-equivalence and establishes
2facd6645599 tuned paper Christian Urban <urbanc@in.tum.de> parents: 1556 diff changeset	78	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	79	also prove strong induction principles that have the usual variable
1566 2facd6645599 tuned paper Christian Urban <urbanc@in.tum.de> parents: 1556 diff changeset	80	convention already built in.
1328 531dcebbf483 start of paper - does not compile yet Christian Urban <urbanc@in.tum.de> parents: 754 diff changeset	81	\end{abstract}
754 b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	82
1493 52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	83
754 b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	84	\input{session}
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	85
1493 52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	86	\bibliographystyle{plain}
52f68b524fd2 slightly more of the paper Christian Urban <urbanc@in.tum.de> parents: 1485 diff changeset	87	\bibliography{root}
754 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	\end{document}
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	90
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	91	%%% Local Variables:
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	92	%%% mode: latex
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	93	%%% TeX-master: t
b85875d65b10 added a paper for possible notes Christian Urban <urbanc@in.tum.de> parents: diff changeset	94	%%% End:

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Mon, 10 May 2010 15:14:02 +0200
changeset 2091	1f38489f1cf0
parent 1961	774d631726ad
child 2216	1a9dbfe04f7d
permissions	-rw-r--r--