--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/LMCS-Paper/document/root.tex	Fri Aug 12 22:37:41 2011 +0200
@@ -0,0 +1,112 @@
+\documentclass{llncs}
+\usepackage{times}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{amssymb}
+%%\usepackage{amsthm}
+\usepackage{tikz}
+\usepackage{pgf}
+\usepackage{pdfsetup}
+\usepackage{ot1patch}
+\usepackage{times}
+\usepackage{boxedminipage}
+\usepackage{proof}
+\usepackage{setspace}
+
+\allowdisplaybreaks
+\urlstyle{rm}
+\isabellestyle{it}
+\renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastyle}{\normalsize\it}%
+
+\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
+\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
+\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\hspace{-0.5mm}\cdot\hspace{-0.5mm}}$}}}
+\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+\renewcommand{\isasymequiv}{$\dn$}
+%%\renewcommand{\isasymiota}{}
+\renewcommand{\isasymxi}{$..$}
+\renewcommand{\isasymemptyset}{$\varnothing$}
+\newcommand{\isasymnotapprox}{$\not\approx$}
+\newcommand{\isasymLET}{$\mathtt{let}$}
+\newcommand{\isasymAND}{$\mathtt{and}$}
+\newcommand{\isasymIN}{$\mathtt{in}$}
+\newcommand{\isasymEND}{$\mathtt{end}$}
+\newcommand{\isasymBIND}{$\mathtt{bind}$}
+\newcommand{\isasymANIL}{$\mathtt{anil}$}
+\newcommand{\isasymACONS}{$\mathtt{acons}$}
+\newcommand{\isasymCASE}{$\mathtt{case}$}
+\newcommand{\isasymOF}{$\mathtt{of}$}
+\newcommand{\isasymAL}{\makebox[0mm][l]{$^\alpha$}}
+\newcommand{\isasymPRIME}{\makebox[0mm][l]{$'$}}
+\newcommand{\isasymFRESH}{\#}
+\newcommand{\LET}{\;\mathtt{let}\;}
+\newcommand{\IN}{\;\mathtt{in}\;}
+\newcommand{\END}{\;\mathtt{end}\;}
+\newcommand{\AND}{\;\mathtt{and}\;}
+\newcommand{\fv}{\mathit{fv}}
+
+\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
+%----------------- theorem definitions ----------
+%%\theoremstyle{plain}
+%%\spnewtheorem{thm}[section]{Theorem}
+%%\newtheorem{property}[thm]{Property}
+%%\newtheorem{lemma}[thm]{Lemma}
+%%\spnewtheorem{defn}[theorem]{Definition}
+%%\spnewtheorem{exmple}[theorem]{Example}
+\spnewtheorem{myproperty}{Property}{\bfseries}{\rmfamily}
+%-------------------- environment definitions -----------------
+\newenvironment{proof-of}[1]{{\em Proof of #1:}}{}
+
+%\addtolength{\textwidth}{2mm}
+\addtolength{\parskip}{-0.33mm}
+\begin{document}
+
+\title{General Bindings and Alpha-Equivalence\\ in Nominal Isabelle}
+\author{Christian Urban and Cezary Kaliszyk}
+\institute{TU Munich, Germany}
+%%%{\{urbanc, kaliszyk\}@in.tum.de}
+\maketitle
+
+\begin{abstract} 
+Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
+prover. It provides a proving infrastructure for reasoning about
+programming language calculi involving named bound variables (as
+opposed to de-Bruijn indices). In this paper we present an extension of
+Nominal Isabelle for dealing with general bindings, that means
+term-constructors where multiple variables are bound at once. Such general
+bindings are ubiquitous in programming language research and only very
+poorly supported with single binders, such as lambda-abstractions. Our
+extension includes new definitions of $\alpha$-equivalence and establishes
+automatically the reasoning infrastructure for $\alpha$-equated terms. We
+also prove strong induction principles that have the usual variable
+convention already built in.
+\end{abstract}
+
+%\category{F.4.1}{subcategory}{third-level}
+
+%\terms
+%formal reasoning, programming language calculi
+
+%\keywords
+%nominal logic work, variable convention
+
+
+\input{session}
+
+\begin{spacing}{0.9}
+  \bibliographystyle{plain}
+  \bibliography{root}
+\end{spacing}
+
+%\pagebreak
+%\input{Appendix} 
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End: