\documentclass[report]{article}

%% Narrow margins
\usepackage{fullpage}

%% Bibtex
\usepackage{natbib}

%% Links
\usepackage{hyperref}

%% -----------------------------------------------------------------------------
%% Commands for Agda
\usepackage[english]{babel}
\usepackage[conor]{agda}
\renewcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathrm{\underline{#1}}}}
\renewcommand{\AgdaFunction}[1]{\textbf{\textcolor{AgdaFunction}{#1}}}
\definecolor{AgdaBound} {HTML}{000000}

\DeclareUnicodeCharacter{9665}{\ensuremath{\lhd}}

%% -----------------------------------------------------------------------------
%% Commands

\newcommand{\mysyn}{\AgdaKeyword}
\newcommand{\mytyc}{\AgdaDatatype}
\newcommand{\myind}{\AgdaInductiveConstructor}
\newcommand{\myfld}{\AgdaField}
\newcommand{\myfun}{\AgdaFunction}
\newcommand{\myb}{\AgdaBound}
\newcommand{\myfield}{\AgdaField}

%% -----------------------------------------------------------------------------

\title{\textsc{Kant}: Implementing Observational Equality}
% TODO remove double @ if we get rid of lhs2TeX
\author{Francesco Mazzoli \href{mailto:fm2209@ic.ac.uk}{\nolinkurl{<fm2209@ic.ac.uk>}}}
\date{June 2013}

\begin{document}

%if False
\begin{code}
module thesis where
open import Level
\end{code}
%endif

\maketitle

\begin{abstract}
  The marriage between programming and logic has been a very fertile one.  In
  particular, since the simply typed lambda calculus (STLC), a number of type
  systems have been devised with increasing expressive power.

  Section \ref{sec:types} will give a very brief overview of STLC, and then
  illustrate how it can be interpreted as a natural deduction system.  Section
  \ref{sec:itt} will introduce Inutitionistic Type Theory (ITT), which expands
  on this concept, employing a more expressive logic.  The exposition is quite
  dense since there is a lot of material to cover; for a more complete treatment
  of the material the reader can refer to \citep{Thompson1991, Pierce2002}.
  Section \ref{sec:equality} will explain why equality has always been a tricky
  business in these theories, and talk about the various attempts that have been
  made to make the situation better.  One interesting development has recently
  emerged: Observational Type theory.

  Section \ref{sec:practical} will describe common extensions found in the
  systems currently in use.  Finally, section \ref{sec:kant} will describe a
  system developed by the author that implements a core calculus based on the
  principles described.
\end{abstract}

\tableofcontents

\section{Simple and not-so-simple types}
\label{sec:types}

\section{Intuitionistic Type Theory and dependent types}
\label{sec:itt}

\section{The struggle for equality}
\label{sec:equality}

\section{A more useful language}
\label{sec:practical}

\section{Kant}
\label{sec:kant}

\appendix

\section{Notation and syntax}

In the languages presented I will also use different fonts and colors for
different things:

\begin{center}
  \begin{tabular}{c | l}
    $\mytyc{Sans}$  & Type constructors. \\
    $\myind{sans}$  & Data constructors. \\
    $\myfld{sans}$  & Field accessors (e.g. \myfld{fst} and \myfld{snd} for products). \\
    $\mysyn{roman}$ & Syntax of the language. \\
    $\myfun{roman}$ & Defined values. \\
    $\myb{math}$    & Bound variables.
  \end{tabular}
\end{center}

\section{Agda rendition of a core ITT}
\label{app:agda-code}

\begin{code}
module ITT where
  data Empty : Set where

  absurd : ∀ {a} {A : Set a} → Empty → A
  absurd ()

  record Unit : Set where
    constructor tt

  record _×_ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
    constructor _,_
    field
      fst : A
      snd : B fst
  open _×_ public

  data Bool : Set where
    true false : Bool

  if_/_then_else_ : ∀ {a} (x : Bool) → (P : Bool → Set a) → P true → P false → P x
  if true / _ then x else _ = x
  if false / _ then _ else x = x

  data W {s p} (S : Set s) (P : S → Set p) : Set (s ⊔ p) where
    _◁_ : (s : S) → (P s → W S P) → W S P

  rec : ∀ {a b} {S : Set a} {P : S → Set b}
    (C : W S P → Set) →      -- some conclusion we hope holds
    ((s : S) →               -- given a shape...
     (f : P s → W S P) →     -- ...and a bunch of kids...
     ((p : P s) → C (f p)) → -- ...and C for each kid in the bunch...
     C (_◁_ s f)) →          -- ...does C hold for the node?
    (x : W S P) →            -- If so, ...
    C x                      -- ...C always holds.
  rec C c (s ◁ f) = c s f (λ p → rec C c (f p))
\end{code}

\nocite{*}
\bibliographystyle{authordate1}
\bibliography{thesis}

\end{document}