top.tex

% $Id: tidbits.tex,v 1.12 2001/03/25 18:02:03 augustss Exp $
%
%\batchmode
\nonstopmode

\documentclass{article}

\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{latexsym}
\usepackage{verbatim}

\newenvironment{code}{\footnotesize\verbatim}{\endverbatim\normalsize}

\date{}
\title{
$\lambda$-calculus cooked four ways
}

\author{
Lennart Augustsson
}

\begin{document}

\maketitle

% ================================================================

\section{Introduction}
This little paper describes how to implement $\lambda$-calculus in
four different ways.  To be precise, it shows how to implement the
functions that compute the ($\beta$) normal form of an expression.
%%% and how to test two expressions for $\alpha$-equality.

\section{Preliminaries}
\subsection{Lambda}
\input{Lambda}
\subsection{IdInt}
\input{IdInt}

\section{Na\"{i}ve Substitution}
\input{Simple}

\section{The Barendregt Convention}
\input{Unique}

\section{Higher Order Abstract Syntax}
\input{HOAS}

\section{deBruijn indicies}
\input{DeBruijn}

\section{Tasting time}
Finally, we want to try out the different implementations.
To this end we have a simple main program to pick which
normal form function to use.

\input{Main}

\end{document}