\documentclass{acmconf}+
−
\usepackage{isabelle}+
−
\usepackage{isabellesym}+
−
\usepackage{amsmath}+
−
\usepackage{amssymb}+
−
\usepackage{tikz}+
−
\usepackage{pgf}+
−
\usepackage{pdfsetup}+
−
\usepackage{ot1patch}+
−
+
−
\urlstyle{rm}+
−
\isabellestyle{it}+
−
+
−
\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}+
−
\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}+
−
\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$}+
−
\newcommand{\LET}{\;\mathtt{let}\;}+
−
\newcommand{\IN}{\;\mathtt{in}\;}+
−
\newcommand{\END}{\;\mathtt{end}\;}+
−
\newcommand{\AND}{\;\mathtt{and}\;}+
−
+
−
+
−
+
−
%----------------- theorem definitions ----------+
−
\newtheorem{property}{Property}[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 convenient reasoning about+
−
programming language calculi involving bound variables that have names (as+
−
opposed to de-Bruijn indices). In this paper we present an extension of+
−
Nominal Isabelle in order to deal with general binding structures. Such+
−
binding structures are ubiquitous in programming language research and only+
−
very poorly supported with single binders, such as the lambdas in the+
−
lambda-calculus. For our extension we introduce novel definitions of+
−
alpha-equivalence and establish automatically the reasoning infrastructure for+
−
alpha-equated terms. This includes strong induction principles that have the+
−
variable convention already built in.+
−
\end{abstract}+
−
+
−
+
−
\input{session}+
−
+
−
\bibliographystyle{plain}+
−
\bibliography{root}+
−
+
−
\end{document}+
−
+
−
%%% Local Variables:+
−
%%% mode: latex+
−
%%% TeX-master: t+
−
%%% End:+
−