\documentclass{acmconf}+ −
\usepackage{isabelle}+ −
\usepackage{isabellesym}+ −
\usepackage{amsmath}+ −
\usepackage{amssymb}+ −
\usepackage{tikz}+ −
\usepackage{pgf}+ −
\usepackage{pdfsetup}+ −
+ −
\urlstyle{rm}+ −
\isabellestyle{it}+ −
+ −
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}+ −
\renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}}+ −
\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}+ −
\renewcommand{\isasymequiv}{$\dn$}+ −
\renewcommand{\isasymiota}{}+ −
\renewcommand{\isasymemptyset}{$\varnothing$}+ −
+ −
+ −
+ −
%----------------- theorem definitions ----------+ −
\newtheorem{Property}{Theorem}[section]+ −
\newtheorem{Theorem}{Theorem}[section]+ −
\newtheorem{Definition}[Theorem]{Definition}+ −
\newtheorem{Example}{\it Example}[section]+ −
+ −
%-------------------- environment definitions -----------------+ −
\newenvironment{example}[0]{\begin{Example} \it}{\end{Example}}+ −
\newenvironment{proof-of}[1]{{\em Proof of #1:}}{}+ −
+ −
+ −
\begin{document}+ −
+ −
\title{\LARGE\bf General Binding Structures in Nominal Isabelle,\\ or How to+ −
Formalise Core-Haskell}+ −
\maketitle+ −
+ −
\maketitle+ −
\begin{abstract} + −
Nominal Isabelle is a definitional extension of the Isabelle/HOL+ −
theorem prover. It provides a proving infrastructure for+ −
conveninet reasoning about programming language calculi. In this paper + −
we present an extension of Nominal Isabelle for dealing with general binding + −
structures. Such structures are ubiquitous in programming language research+ −
and only very poorly handled by the well-known single abstraction in the+ −
lambda-calculus. We give definitions for alpha-equivalence and establish+ −
the reasoning structure for alpha-equated terms. For example we provide+ −
a strong induction principle that has the variable convention already+ −
built in.+ −
\end{abstract}+ −
+ −
+ −
\input{session}+ −
+ −
\bibliographystyle{plain}+ −
\bibliography{root}+ −
+ −
\end{document}+ −
+ −
%%% Local Variables:+ −
%%% mode: latex+ −
%%% TeX-master: t+ −
%%% End:+ −