\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:+ −