--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Pearl/document/root.tex	Sat Apr 03 21:53:04 2010 +0200
@@ -0,0 +1,63 @@
+\documentclass[runningheads]{llncs}
+\usepackage{times}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{longtable}
+
+
+\usepackage{pdfsetup}
+\urlstyle{rm}
+\isabellestyle{it}
+\renewcommand{\isastyle}{\isastyleminor}
+\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}}
+\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+\renewcommand{\isasymequiv}{$\dn$}
+\renewcommand{\isasymiota}{}
+\renewcommand{\isasymrightleftharpoons}{}
+\renewcommand{\isasymemptyset}{$\varnothing$}
+
+\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
+
+
+\begin{document}
+
+\title{Proof Pearl: A New Foundation for Nominal Isabelle}
+\author{Brian Huffman\inst{1} and Christian Urban\inst{2}}
+\institute{Portland State University \and Technical University of Munich}
+\maketitle
+
+\begin{abstract}
+Pitts et al introduced a beautiful theory about names and binding based on the
+notions of permutation and support. The engineering challenge is to smoothly
+adapt this theory to a theorem prover environment, in our case Isabelle/HOL.
+We present a formalisation of this work that differs from our earlier approach
+in two important respects: First, instead of representing permutations as
+lists of pairs of atoms, we now use a more abstract representation based on
+functions.  Second, whereas the earlier work modeled different sorts of atoms
+using different types, we now introduce a unified atom type that includes all
+sorts of atoms. Interestingly, we allow swappings, that is permutations build up by
+two atoms, to be ill-sorted.  As a result of these design changes, we can iron
+out inconveniences for the user, considerably simplify proofs and also
+drastically reduce the amount of custom ML-code. Furthermore we can extend the
+capabilities of Nominal Isabelle to deal with variables that carry additional
+information. We end up with a pleasing and formalised theory of permutations
+and support, on which we can build an improved and more powerful version of
+Nominal Isabelle.
+\end{abstract}
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End: