thesis stub

6 files changed, 734 insertions, 39 deletions

diff --git a/InterimReport.agda b/InterimReport.agda
index c433d59..839060f 100644
--- a/InterimReport.agda
+++ b/InterimReport.agda
@@ -147,4 +147,4 @@ module Ext where
 
   map-#==#-map' : forall {A B C} (f : B -> C) (g : A -> B) ->
                   map (f # g) == (map f # map g)
-  map-#==#-map' f g = ext (map-#==#-map f g)
\ No newline at end of file
+  map-#==#-map' f g = ext (map-#==#-map f g)
diff --git a/InterimReport.tex b/InterimReport.tex
index 752288c..1c89260 100644
--- a/InterimReport.tex
+++ b/InterimReport.tex
@@ -36,6 +36,7 @@
 \usepackage{turnstile}
 \usepackage{centernot}
 \usepackage{stmaryrd}
+\usepackage{bm}
 
 %% -----------------------------------------------------------------------------
 %% Utils
@@ -170,7 +171,7 @@ In the languages presented I will also use different fonts for different things:
 
 Moreover, I will from time to time give examples in the Haskell programming
 language as defined in \citep{Haskell2010}, which I will typeset in
-\texttt{typewriter} font.  I assume that the reader is already familiar with
+\texttt{teletype} font.  I assume that the reader is already familiar with
 Haskell, plenty of good introductions are available \citep{LYAH,ProgInHask}.
 
 \subsection{Untyped $\lambda$-calculus}
@@ -224,8 +225,21 @@ complete.  As a corollary, we must be able to devise a term that reduces forever
   \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \app{(\abs{x}{\app{x}{x}})}{(\abs{x}{\app{x}{x}})} \bred \dotsb
 \]
 Terms that can be reduced only a finite number of times (the non-looping ones)
-are said to be \emph{normalising}, and the `final' term (where no reductions are
-possible on the term or on its subterms) is called \emph{normal form}.
+are said to be \emph{strongly normalising}, and the `final' term (where no
+reductions are possible on the term or on its subterms) is called \emph{normal
+  form}.
+
+From now on I will omit the `strongly' in `strongly normalising', however weaker
+notions of normalisation have been described.  More generally, it is often
+convenient not to reduce subterms indiscriminately, and have a more principled
+approach to evaluation, or `evaluation strategy'.  Common evaluation strategies
+include `call by value' (or `strict'), where arguments of abstractions are
+reduced before being applied to the abstraction; and conversely `call by name'
+(or `lazy'), where we reduce only when we need to do so to proceed - in other
+words when we have an application where the function is still not a $\lambda$.
+In both these reduction strategies we never reduce under an abstraction, and a
+different notion of normalisation (`weak head normal form') if often used, where
+every abstraction is a weak head normal form.
 
 \subsection{The simply typed $\lambda$-calculus}
 \label{sec:stlc}
@@ -245,21 +259,27 @@ The syntax for types is as follows:
 
 \begin{center}
   \axname{syntax}
-   $$\tysyn ::= x \separ \tysyn \tyarr \tysyn$$
+$$
+\begin{array}{rcl}
+  \tysyn & ::= & \alpha \separ \tysyn \tyarr \tysyn \\
+  \alpha & \in & \text{A set of base types provided by the language}
+\end{array}
+$$
 \end{center}
 
-I will use $\tya,\tyb,\dots$ to indicate a generic type.
+I will use $\tya,\tyb,\dots$ to indicate a generic type, carrying the convention
+from set theory of denoting member of sets with lowercase letters and sets
+themselves with capitals.
 
 A context $\Gamma$ is a map from variables to types.  I will use the notation
 $\Gamma; x : \tya$ to augment it and to `extract' pairs from it.
 
 Predictably, $\tya \tyarr \tyb$ is the type of a function from $\tya$ to
-$\tyb$.  We need to be able to decorate our abstractions with
-types\footnote{Actually, we don't need to: computers can infer the right type
-  easily, but that is another story.}:
+$\tyb$.  We extend the syntax and allow to decorate our abstractions with
+types:
 \begin{center}
   \axname{syntax}
-   $$\termsyn ::= x \separ (\abs{x : \tysyn}{\termsyn}) \separ (\app{\termsyn}{\termsyn})$$
+   $$\termsyn ::= x \separ (\abs{x{:}\tysyn}{\termsyn}) \separ (\app{\termsyn}{\termsyn})$$
 \end{center}
 Now we are ready to give the typing judgements:
 
@@ -273,7 +293,7 @@ Now we are ready to give the typing judgements:
     \DisplayProof
     &
     \AxiomC{$\Gamma; x : \tya \vdash \termt : \tyb$}
-    \UnaryInfC{$\Gamma \vdash \abs{x : \tya}{\termt} : \tya \tyarr \tyb$}
+    \UnaryInfC{$\Gamma \vdash \abs{x{:}\tya}{\termt} : \tya \tyarr \tyb$}
     \DisplayProof
   \end{tabular}
 
@@ -344,10 +364,11 @@ That is, function composition.  We might want extend our bare lambda calculus
 with a couple of terms former to make our natural deduction more pleasant to
 use.  For example, tagged unions (\texttt{Either} in Haskell) are disjunctions,
 and tuples (or products) are conjunctions.  We also want to be able to express
-falsity ($\bot$): that can done by introducing a type inhabited by no terms.  If
-evidence of such a type is presented, then we can derive any type, which
-expresses absurdity.  Conversely, truth ($\top$) is the type with just one
-trivial element ($\lcunit$).
+falsity ($\bot$): that can done by introducing a type inhabited by no closed
+terms.  If evidence of such a type is presented (necessarily under an
+abstraction), then we can derive any type, which expresses absurdity.
+Conversely, truth ($\top$) is the type with just one trivial element
+($\lcunit$).
 
 \newcommand{\lcinl}{\lccon{inl}\appsp}
 \newcommand{\lcinr}{\lccon{inr}\appsp}
@@ -364,7 +385,7 @@ trivial element ($\lcunit$).
 \newcommand{\lcabsurd}{\lcfun{absurd}\appsp}
 \newcommand{\lcabsurdd}[1]{\lcfun{absurd}_{#1}\appsp}
 
-
+% TODO make parens bold with \bm
 \begin{center}
   \axname{syntax}
   $$
@@ -507,10 +528,11 @@ above additions, and thus would sit where $\lambda{C}$ sits in the
 
 Logic frameworks and programming languages based on type theory have a long
 history.  Per Martin-L\"{o}f described the first version of his theory in 1971,
-but then revised it since the original version was too impredicative and thus
-inconsistent\footnote{In the early version $\lcsetz : \lcsetz$, see section
-  \ref{sec:core-tt} for an explanation on why this causes problems.}.  For this
-reason he gave a revised and consistent definition later \citep{Martin-Lof1984}.
+but then revised it since the original version was inconsistent due to its
+impredicativity\footnote{In the early version there was only one universe
+  $\lcsetz$ and $\lcsetz : \lcsetz$, see section \ref{sec:core-tt} for an
+  explanation on why this causes problems.}.  For this reason he gave a revised
+and consistent definition later \citep{Martin-Lof1984}.
 
 A related development is the polymorphic $\lambda$-calculus, and specifically
 the previously mentioned System F, which was developed independently by Girard
@@ -631,11 +653,12 @@ logic. $\tyarr$ and $\times$ are at the core of the machinery of ITT:
 
 \begin{description}
 \item[`forall' ($\tyarr$)] is a generalisation of $\tyarr$ in the STLC and
-  expresses universal quantification in our logic.  It is often written with a
-  syntax closer to logic, e.g. $\forall x : \tya. \tyb$.  In the
-  literature this is also known as `dependent product' and shown as $\Pi$,
-  following the interpretation of functions as infinitary products. I will just
-  call it `dependent function', reserving `product' for $\exists$.
+  expresses universal quantification in our logic, where $A \tyarr B$ can be
+  expressed as $(- : A) \tyarr B$.  It is often written with a syntax closer to
+  logic, e.g. $\forall x : \tya. \tyb$.  In the literature this is also known as
+  `dependent product' and shown as $\Pi$, following the interpretation of
+  functions as infinitary products. I will just call it `dependent function',
+  reserving `product' for $\exists$.
 
 \item[`exists' ($\times$)] is a generalisation of $\wedge$ in the extended STLC
   of section \ref{sec:curry-howard}, and thus I will call it `dependent
@@ -643,8 +666,8 @@ logic. $\tyarr$ and $\times$ are at the core of the machinery of ITT:
   logic, it represents existential quantification.  Similarly to $\tyarr$, it is
   often written as $\exists x : \tya. \tyb$.
 
-  For added confusion, in the literature that calls $\tyarr$ $\Pi$, $\times$ is
-  often named `dependent sum' and shown as $\Sigma$.  This is following the
+  For added confusion, in the literature that uses $\Pi$ for $\tyarr$, $\times$
+  is often named `dependent sum' and shown as $\Sigma$.  This is following the
   interpretation of $\exists$ as a generalised, infinitary $\vee$, where the
   first element of the pair is the `tag' that determines which type the second
   element will have.
@@ -655,12 +678,12 @@ create functions that accept and return types.  For this reason we define
 $\defeq$ as the smallest equivalence relation extending $\bredc$, where $\bredc$
 is the reflexive transitive closure of $\bred$; and we treat types that are
 related according to $\defeq$ as the same.  Another way of seeing $\defeq$ is
-this: when we want to compare two types for equality, we reduce them as far as
+this: when we want to compare two terms for equality, we reduce them as far as
 possible and then check if they are equal\footnote{Note that when comparing
-  terms we do it up to $\alpha$-renaming.  That is, we do not consider
-  relabelling of variables as a difference - for example $\abs{x : A}{x} \defeq
-  \abs{y : A}{y}$.}.  This works since not only each term has a normal form (ITT
-is strongly normalising), but the normal form is also unique; or in other words
+  terms we do it up to $\alpha$-renaming.  That is, we do not consider renaming
+  of bound variables as a difference - for example $\abs{x : A}{x} \defeq \abs{y
+    : A}{y}$.}.  This works since not only each term has a normal form (ITT is
+strongly normalising), but the normal form is also unique; or in other words
 $\bred$ is confluent (if $\termt \bredc \termm$ and $\termt \bredc \termn$, then
 there is a $p$ such that $\termm \bredc \termp$ and $\termn \bredc \termp$).
 This measure makes sure that, for instance, $\app{(\abs{x :
@@ -669,13 +692,13 @@ and will be analysed better in section \ref{sec:equality}.
 
 The theory presented is \emph{stratified}.  We have a hierarchy of types
 $\lcset{0} : \lcset{1} : \lcset{2} : \dots$, so that there is no `type of all
-types', and our theory is predicative.  Type-formers like $\tyarr$ and $\times$
+types', and our theory is predicative.  Constructors like $\tyarr$ and $\times$
 take the least upper bound $\sqcup$ of the contained types. The layers of the
 hierarchy are called `universes'.  Theories where $\lcsetz : \lcsetz$ are
 inconsistent due to Girard's paradox \citep{Hurkens1995}, and thus lose their
-well-behavedness.  Some impredicativity sometimes has its place, either because
-the theory retain good properties (normalization, consistency, etc.) anyway,
-like in System F and CoC; or because we are at a stage at which we do not care.
+well-behavedness.  Impredicativity sometimes has its place, either because the
+theory retain good properties (normalization, consistency, etc.) anyway, like in
+System F and CoC; or because we are at a stage at which we do not care.
 
 \subsection{Base Types}
 \label{sec:base-types}
diff --git a/Makefile b/Makefile
index 1514e88..ad3f550 100644
--- a/Makefile
+++ b/Makefile
@@ -1,8 +1,22 @@
-SOURCES = $(wildcard *.tex)
-OBJECTS = $(patsubst %.tex, %.pdf, $(SOURCES))
+SOURCEST = $(wildcard *.tex)
+OBJECTST = $(patsubst %.tex, %.pdf, $(SOURCEST))
+SOURCESA = $(wildcard *.lagda)
+OBJECTSA = $(patsubst %.lagda, %.pdf, $(SOURCESA))
+OBJECTS = $(OBJECTST) $(OBJECTSA)
 
 all: $(OBJECTS)
 
+thesis.pdf: thesis.tex thesis.bib agda.sty
+	pdflatex -halt-on-error $< -o $@
+	bibtex thesis
+	pdflatex -halt-on-error $< -o $@
+	pdflatex -halt-on-error $< -o $@
+
+agda.sty: thesis.tex
+
+thesis.tex: thesis.lagda
+	agda --latex --latex-dir . -i . -i ~/src/agda-lib/src/ thesis.lagda
+
 InterimReport.pdf: InterimReport.tex InterimReport.bib InterimReport.agda
 	xelatex -halt-on-error $< -o $@
 	bibtex InterimReport
@@ -15,6 +29,8 @@ idris-proposal.pdf: idris-proposal.tex
 
 clean: cleanup
 	rm -f $(OBJECTS)
+	rm -f thesis.tex agda.sty
 
 cleanup:
-	rm -f *.log *.aux *.nav *.snm *.toc *.vrb *.out *.bbl *.blg
+	rm -f *.log *.aux *.nav *.snm *.toc *.vrb *.out *.bbl *.blg *.agdai
+
diff --git a/thesis.bib b/thesis.bib
new file mode 100644
index 0000000..9519f9f
--- /dev/null
+++ b/thesis.bib
@@ -0,0 +1,314 @@
+@inbook{Thompson1991,
+  author = {Thompson, Simon},
+  title = {Type Theory and Functional Programming},
+  publisher = {Addison-Wesley},
+  year = {1991}
+}
+
+@inbook{Pierce2002,
+  author = {Pierce, Benjamin C.},
+  title = {Types and Programming Languages},
+  publisher = {The MIT Press},
+  year = {2002}
+}
+
+@online{Coq,
+  author = {{The Coq Team}},
+  title = {The Coq Proof Assistant},
+  url = {\url{coq.inria.fr}},
+  howpublished = {\url{http://coq.inria.fr}},
+  year = 2013
+}
+
+@online{GHC,
+  author = {{The GHC Team}},
+  title = {The Glorious Glasgow Haskell Compilation System User's Guide, Version 7.6.1},
+  url = {http://www.haskell.org/ghc/docs/7.6.1/html/users_guide/},
+  howpublished = {\url{http://www.haskell.org/ghc/docs/latest/html/users_guide/}},
+  year = 2012
+}
+
+@online{EpigramTut,
+  author = {Conor McBride},
+  title = {Epigram: Practical Programming with Dependent Types},
+  url = {http://strictlypositive.org/epigram-notes.ps.gz},
+  howpublished = {\url{http://strictlypositive.org/epigram-notes.ps.gz}},
+  year = 2004
+}
+
+@online{Haskell2010,
+  author = {Simon Marlow},
+  title = {Haskell 2010, Language Report},
+  url = {http://www.haskell.org/onlinereport/haskell2010/},
+  howpublished = {\url{http://www.haskell.org/onlinereport/haskell2010/}},
+  year = 2010
+}
+
+@online{LYAH,
+  author = {Miran Lipova\v{c}a},
+  title = {Learn You a Haskell for Great Good!},
+  url = {http://learnyouahaskell.com/},
+  howpublished = {\url{http://learnyouahaskell.com/}},
+  year = 2009
+}
+
+@inbook{ProgInHask,
+  author = {Graham Hutton},
+  title = {Programming in Haskell},
+  year = 2007,
+  publisher = {Cambridge University Press}
+}
+
+@inbook{NuPRL,
+  author = {Robert L. Constable and the PRL Group},
+  title = {Implementing Mathematics with The NuPRL Proof Development System},
+  year = 1986,
+  publisher = Prentice-Hall
+}
+
+
+@article{Altenkirch2010,
+author = {Altenkirch, Thorsten and Danielsson, N and L\"{o}h, A and Oury, Nicolas},
+file = {:home/bitonic/docs/papers/PiSigma.pdf:pdf},
+journal = {Functional and Logic \ldots},
+number = {Sheard 2005},
+title = {{$\Pi$$\Sigma$: dependent types without the sugar}},
+url = {http://www.springerlink.com/index/91W712G2806R575H.pdf},
+year = {2010}
+}
+@article{Altenkirch2007,
+address = {New York, New York, USA},
+author = {Altenkirch, Thorsten and McBride, Conor and Swierstra, Wouter},
+doi = {10.1145/1292597.1292608},
+file = {:home/bitonic/docs/papers/OTT2.pdf:pdf},
+isbn = {9781595936776},
+journal = {Proceedings of the 2007 workshop on Programming languages meets program verification - PLPV '07},
+keywords = {case analysis relies on,datatypes are indexed in,equality,of any language where,ole in the programs,play a crucial internal,rˆ,solving,some way,type theory},
+pages = {57},
+publisher = {ACM Press},
+title = {{Observational equality, now!}},
+url = {http://portal.acm.org/citation.cfm?doid=1292597.1292608},
+year = {2007}
+}
+@article{Barendregt1991,
+author = {Barendregt, Henk},
+file = {:home/bitonic/docs/papers/lambda-cube.pdf:pdf},
+journal = {Journal of functional programming},
+title = {{Introduction to generalized type systems}},
+url = {http://www.diku.dk/hjemmesider/ansatte/henglein/papers/barendregt1991.pdf},
+year = {1991}
+}
+@article{Bove2009,
+author = {Bove, Ana and Dybjer, Peter and Norell, Ulf},
+file = {:home/bitonic/docs/papers/agda-overview.pdf:pdf},
+journal = {Theorem Proving in Higher Order Logics},
+title = {{A brief overview of Agda - a functional language with dependent types}},
+url = {http://www.springerlink.com/index/h12lq70470983732.pdf},
+year = {2009}
+}
+@article{Brady2012,
+author = {Brady, Edwin},
+file = {:home/bitonic/docs/papers/idris-implementation.pdf:pdf},
+journal = {Unpublished draft},
+number = {November},
+title = {{Implementing General Purpose Dependently Typed Programming Languages}},
+url = {http://www.cs.st-andrews.ac.uk/~eb/drafts/impldtp.pdf},
+year = {2012}
+}
+@article{Chapman2010,
+address = {New York, New York, USA},
+author = {Chapman, James and Dagand, Pierre-\'{E}variste and McBride, Conor and Morris, Peter},
+doi = {10.1145/1863543.1863547},
+file = {:home/bitonic/docs/papers/conor-levitation.pdf:pdf},
+isbn = {9781605587943},
+journal = {Proceedings of the 15th ACM SIGPLAN international conference on Functional programming - ICFP '10},
+pages = {3},
+publisher = {ACM Press},
+title = {{The gentle art of levitation}},
+url = {http://portal.acm.org/citation.cfm?doid=1863543.1863547},
+year = {2010}
+}
+@article{Church1936,
+author = {Church, Alonzo},
+file = {:home/bitonic/docs/papers/church-lc.pdf:pdf},
+journal = {American journal of mathematics},
+number = {2},
+pages = {345--363},
+title = {{An unsolvable problem of elementary number theory}},
+url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2371045},
+volume = {58},
+year = {1936}
+}
+@article{Church1940,
+author = {Church, Alonzo},
+file = {:home/bitonic/docs/papers/church-stlc.pdf:pdf},
+journal = {J. Symb. Log.},
+number = {2},
+pages = {56--68},
+title = {{A formulation of the simple theory of types}},
+url = {http://www.ams.org/leavingmsn?url=http://dx.doi.org/10.2307/2266170},
+volume = {5},
+year = {1940}
+}
+@article{Coquand1986,
+author = {Coquand, Thierry and Huet, Gerard},
+file = {:home/bitonic/docs/papers/coc.pdf:pdf},
+title = {{The calculus of constructions}},
+url = {http://hal.inria.fr/docs/00/07/60/24/PDF/RR-0530.pdf},
+year = {1986}
+}
+@article{Curry1934,
+author = {Curry, Haskell B.},
+file = {:home/bitonic/docs/papers/curry-stlc.pdf:pdf},
+journal = {Proceedings of the National Academy of Sciences of the United States of America},
+number = {1930},
+pages = {584--590},
+title = {{Functionality in combinatory logic}},
+url = {http://www.ncbi.nlm.nih.gov/pmc/articles/pmc1076489/},
+volume = {511},
+year = {1934}
+}
+@article{Dybjer1991,
+author = {Dybjer, Peter},
+file = {:home/bitonic/docs/papers/dybjer-inductive.ps:ps},
+journal = {Logical Frameworks},
+title = {{Inductive sets and families in Martin-L\"{o}f's type theory and their set-theoretic semantics}},
+url = {http://books.google.com/books?hl=en\&lr=\&id=X9wfWwslFQIC\&oi=fnd\&pg=PA280\&dq=Inductive+Sets+and+Families+in+Martin-L\%C3\%B6f\%27s+Type+Theory+and+Their+Set-Theoretic+Semantics\&ots=LewzM17GcW\&sig=vF4GgtlEBSf1uwRV1o\_unDtLats},
+year = {1991}
+}
+@article{Hurkens1995,
+author = {Hurkens, Antonius J.C.},
+file = {:home/bitonic/docs/papers/hurkens-paradox.pdf:pdf},
+journal = {Typed Lambda Calculi and Applications},
+title = {{A simplification of Girard's paradox}},
+url = {http://www.springerlink.com/index/W718604JN467672H.pdf},
+year = {1995}
+}
+@article{Jacobs1997,
+author = {Jacobs, Bart and Rutten, Jan},
+file = {:home/bitonic/docs/papers/coalgebra-coind.pdf:pdf},
+journal = {EATCS Bulletin},
+number = {1997},
+title = {{A tutorial on (co) algebras and (co) induction}},
+url = {http://synrc.com/publications/cat/Logic/CoinductionCoalgebrasTutorial.pdf},
+volume = {62},
+year = {1997}
+}
+@book{Martin-Lof1984,
+author = {Martin-L\"{o}f, Per},
+file = {:home/bitonic/docs/papers/martin-lof-tt.pdf:pdf},
+isbn = {8870881059},
+publisher = {Bibliopolis},
+title = {{Intuitionistic type theory}},
+year = {1984}
+}
+@article{McBride2004,
+author = {McBride, Conor},
+doi = {10.1017/S0956796803004829},
+file = {:home/bitonic/docs/papers/view-from-the-left.ps.gz:gz},
+journal = {Journal of Functional Programming},
+month = jan,
+number = {1},
+pages = {69--111},
+title = {{The View from The Left}},
+url = {http://strictlypositive.org/view.ps.gz},
+volume = {14},
+year = {2004}
+}
+@phdthesis{Norell2007,
+author = {Norell, Ulf},
+file = {:home/bitonic/docs/papers/ulf-thesis.pdf:pdf},
+isbn = {9789172919969},
+school = {Chalmers University of Technology and G\"{o}teborg University},
+title = {{Towards a practical programming language based on dependent type theory}},
+url = {http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf},
+year = {2007}
+}
+@article{Oury2008,
+address = {New York, New York, USA},
+author = {Oury, Nicolas and Swierstra, Wouter},
+doi = {10.1145/1411204.1411213},
+file = {:home/bitonic/docs/papers/powerofpi.pdf:pdf},
+isbn = {9781595939197},
+journal = {Proceeding of the 13th ACM SIGPLAN international conference on Functional programming - ICFP '08},
+pages = {39},
+publisher = {ACM Press},
+title = {{The power of Pi}},
+url = {http://portal.acm.org/citation.cfm?doid=1411204.1411213},
+year = {2008}
+}
+@article{Pierce2000,
+author = {Pierce, Benjamin C. and Turner, David N.},
+doi = {10.1145/345099.345100},
+file = {:home/bitonic/docs/papers/local-type-inference.pdf:pdf},
+issn = {01640925},
+journal = {ACM Transactions on Programming Languages and Systems},
+month = jan,
+number = {1},
+pages = {1--44},
+title = {{Local type inference}},
+url = {http://portal.acm.org/citation.cfm?doid=345099.345100},
+volume = {22},
+year = {2000}
+}
+@article{Pollack1990,
+author = {Pollack, Robert},
+file = {:home/bitonic/docs/papers/implicit-syntax.ps:ps},
+journal = {Informal Proceedings of First Workshop on Logical Frameworks},
+title = {{Implicit syntax}},
+url = {http://reference.kfupm.edu.sa/content/i/m/implicit\_syntax\_\_1183660.pdf},
+year = {1992}
+}
+@article{Reynolds1994,
+author = {Reynolds, John C.},
+file = {:home/bitonic/docs/papers/reynolds-polymorphic-lc.ps:ps},
+journal = {Logical Foundations of Functional Programming},
+title = {{An introduction to the polymorphic lambda calculus}},
+url = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.7.9916\&rep=rep1\&type=pdf},
+year = {1994}
+}
+@article{Sulzmann2007,
+address = {New York, New York, USA},
+author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and Jones, Simon Peyton and Donnelly, Kevin},
+doi = {10.1145/1190315.1190324},
+file = {:home/bitonic/docs/papers/systemf-coercions.pdf:pdf},
+isbn = {159593393X},
+journal = {Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation - TLDI '07},
+pages = {53},
+publisher = {ACM Press},
+title = {{System F with type equality coercions}},
+url = {http://portal.acm.org/citation.cfm?doid=1190315.1190324},
+year = {2007}
+}
+@article{Vytiniotis2011,
+author = {Vytiniotis, Dimitrios and Jones, Simon Peyton and Schrijvers, Tom and Sulzmann, Martin},
+file = {:home/bitonic/docs/papers/outsidein.pdf:pdf},
+journal = {Journal of Functional Programming},
+number = {4-5},
+pages = {333--412},
+title = {{OutsideIn (X) Modular type inference with local assumptions}},
+url = {http://journals.cambridge.org/production/action/cjoGetFulltext?fulltextid=8274818},
+volume = {21},
+year = {2011}
+}
+@article{Yorgey2012,
+address = {New York, New York, USA},
+author = {Yorgey, Brent a. and Weirich, Stephanie and Cretin, Julien and {Peyton Jones}, Simon and Vytiniotis, Dimitrios and Magalh\~{a}es, Jos\'{e} Pedro},
+doi = {10.1145/2103786.2103795},
+file = {:home/bitonic/docs/papers/haskell-promotion.pdf:pdf},
+isbn = {9781450311205},
+journal = {Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation - TLDI '12},
+pages = {53},
+publisher = {ACM Press},
+title = {{Giving Haskell a promotion}},
+url = {http://dl.acm.org/citation.cfm?doid=2103786.2103795},
+year = {2012}
+}
+@phdthesis{McBride1999,
+author = {McBride, Conor},
+file = {:home/bitonic/docs/papers/conorthesis.pdf:pdf},
+school = {University of Edinburgh},
+title = {{Dependently typed functional programs and their proofs}},
+url = {http://lac-repo-live7.is.ed.ac.uk/handle/1842/374},
+year = {1999}
+}
diff --git a/thesis.lagda b/thesis.lagda
new file mode 100644
index 0000000..985c611
--- /dev/null
+++ b/thesis.lagda
@@ -0,0 +1,153 @@
+\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}
diff --git a/thesis.ptb b/thesis.ptb
new file mode 100644
index 0000000..77d5935
--- /dev/null
+++ b/thesis.ptb
@@ -0,0 +1,189 @@
+\def\PTtemp{..}\empty
+\def\PTtemp{..}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{4.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{4.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{4.}\empty
+\def\PTtemp{6}\empty
+\def\PTtemp{6.}\empty
+\def\PTtemp{6}\empty
+\def\PTtemp{6.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{4.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{4.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{29}\empty
+\def\PTtemp{29.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{29}\empty
+\def\PTtemp{29.}\empty
+\def\PTtemp{5}\empty
+\def\PTtemp{29}\empty
+\def\PTtemp{29.}\empty
+\def\PTtemp{5}\empty
+\def\PTtemp{5.}\empty
+\def\PTtemp{5}\empty
+\def\PTtemp{29}\empty
+\def\PTtemp{29.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{29}\empty
+\def\PTtemp{29.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{29}\empty
+\def\PTtemp{29.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{..}\empty
+\def\PTtemp{..}\empty
+\def\PTtemp{..}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{4.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{4.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{4.}\empty
+\def\PTtemp{6}\empty
+\def\PTtemp{6.}\empty
+\def\PTtemp{6}\empty
+\def\PTtemp{6.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{4.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{4.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{29}\empty
+\def\PTtemp{29.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{29}\empty
+\def\PTtemp{29.}\empty
+\def\PTtemp{5}\empty
+\def\PTtemp{29}\empty
+\def\PTtemp{29.}\empty
+\def\PTtemp{5}\empty
+\def\PTtemp{5.}\empty
+\def\PTtemp{5}\empty
+\def\PTtemp{29}\empty
+\def\PTtemp{29.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{29}\empty
+\def\PTtemp{29.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{29}\empty
+\def\PTtemp{29.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{..}\empty
+\def\PTtemp{..}\empty
+\def\PTtemp{..}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{4.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{4.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{4.}\empty
+\def\PTtemp{6}\empty
+\def\PTtemp{6.}\empty
+\def\PTtemp{6}\empty
+\def\PTtemp{6.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{4.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{4.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{29}\empty
+\def\PTtemp{29.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{29}\empty
+\def\PTtemp{29.}\empty
+\def\PTtemp{5}\empty
+\def\PTtemp{29}\empty
+\def\PTtemp{29.}\empty
+\def\PTtemp{5}\empty
+\def\PTtemp{5.}\empty
+\def\PTtemp{5}\empty
+\def\PTtemp{29}\empty
+\def\PTtemp{29.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{29}\empty
+\def\PTtemp{29.}\empty
+\def\PTtemp{4}\empty
+\def\PTtemp{29}\empty
+\def\PTtemp{29.}\empty
+\def\PTtemp{2}\empty
+\def\PTtemp{2.}\empty
+\def\PTtemp{..}\empty