report.tex

\documentclass[12pt,a4paper]{article}
\input{latexmacros.tex}

%packages
\usepackage{bussproofs}
\usepackage{amsmath}
\usepackage{tikz-cd}
\usepackage{comment}

%commands
\newcommand{\proves}{\vdash}
\renewcommand{\succ}{\textbf{succ}}
\newcommand{\pred}{\textbf{pred}}
\newcommand{\iszero}{\textbf{iszero}}
\newcommand{\T}{\textbf{T}}
\newcommand{\F}{\textbf{F}}
\newcommand{\Y}{\textbf{Y}}
\newcommand{\zero}{\textbf{zero}}


\title{Implementing PCF in Idris}
\author{Alex Keizer \and Jeremy Kirn \and Simon Lemal}
\date{\today}
\hypersetup{pdfauthor={Alex Keizer, Jeremy Kirn, Simon Lemal}, pdftitle={Implementing PCF in Idris}}

\begin{document}

\maketitle

\begin{abstract}
PCF is a small extension of the simply typed lambda calculus that can be thought of as a basic programming language. We give a brief introduction to PCF, including its small-step reduction rules, and then give the details of two of our implementations of PCF in Idris, a dependently typed programming language similar to Haskell. The second implementation more heavily utilizes the dependent types of Idris.

%We give a toy example of a report in \emph{literate programming} style.
%The main advantage of this is that source code and documentation can
%be written and presented next to each other.
%We use the listings package to typeset Idris source code nicely.
\end{abstract}


\setcounter{tocdepth}{2}
\tableofcontents



% We include one file for each section. The ones containing code should
% be called something.lhs and also mentioned in the .cabal file.

\input{PCF}

\input{PrimeImpl}

\input{TypedImpl}

\addcontentsline{toc}{section}{Bibliography}
\bibliographystyle{alpha}
\bibliography{references.bib}  % display URLs

\end{document}