+Functional programming is in good shape. In particular the `well-typed'
+line of work originating from Milner's ML has been extremely fruitful,
+in various directions. Nowadays functional, well-typed programming
+languages like Haskell or OCaml are slowly being absorbed by the
+mainstream. An important related development---and in fact the original
+motivator for ML's existence---is the advancement of the practice of
+\emph{interactive theorem provers}.
+
+
+An interactive theorem prover, or proof assistant, is a tool that lets
+the user develop formal proofs with the confidence of the machine
+checking it for correctness. While the effort towards a full
+formalisation of mathematics has been ongoing for more than a century,
+theorem provers have been the first class of software whose
+implementation depends directly on these theories.
+
+In a fortunate turn of events, it was discovered that well-typed
+functional programming and proving theorems in an \emph{intuitionistic}
+logic are the same activity. Under this discipline, the types in our
+programming language can be interpreted as proposition in our logic; and
+the programs implementing the specification given by the types as their
+proofs. This fact stimulated a very active transfer of techniques and
+knowledge between logic and programming language theory, in both
+directions.
+
+Mathematics could provide programming with a huge wealth of abstractions
+and constructs developed over centuries. Moreover, identifying our
+types with a logic lets us focus on foundational questions regarding
+programming with a much more solid approach, given the years of rigorous
+study of logic. Programmers, on the other hand, had already developed a
+wealth of approaches to effectively collaborate with computers, through
+the study of programming languages.
+
+We will follow the discipline of Intuitionistic Type Theory, or
+Martin-L\"{o}f Type Theory, after its inventor. First formulated in the
+70s and then adjusted through a series of revisions, it has endured as
+the core of many practical systems widely in use today, and it is
+probably the most prominent instance of the proposition-as-types and
+proofs-as-programs discipline. One of the most debated subjects in this
+field has been regarding what notion of \emph{equality} should be
+exposed to the user.
+
+The tension in the field of equality springs from the fact that there is
+a divide between what the user can prove equal \emph{inside} the
+theory---what is \emph{propositionally} equal--- and what the theorem
+prover identifies as equal in its meta-theory---what is
+\emph{definitionally} equal. If we want our system to be well behaved
+(for example if we want type checking to be decidable) we must keep the
+two notions separate, with definitional equality inducing propositional
+equality, but not the reverse. However in this scenario propositional
+equality is weaker than we would like: we can only prove terms equal
+based on their syntactical structure, and not based on their observable
+behaviour.
+
+This thesis is concerned with exploring a new approach in this area,
+\emph{observational} equality. Promising to provide a more adequate
+propositional equality while retaining well-behavedness, it still is a
+relatively unexplored notion. We set ourselves to change that by
+studying it in a setting more akin the one found in currently available
+theorem provers.
+
+\subsection{Structure}
+
+Section \ref{sec:types} will give a brief overview of the
+$\lambda$-calculus, both typed and untyped. This will give us the
+chance to introduce most of the concepts mentioned above rigorously, and
+gain some intuition about them. An excellent introduction to types in
+general can be found in \cite{Pierce2002}, although not from the
+perspective of theorem proving.
+
+Section \ref{sec:itt} will describe a set of basic construct that form a
+`baseline' Intuitionistic Type Theory. The goal is to familiarise with
+the main concept of ITT before attacking the problem of equality. Given
+the wealth of material covered the exposition is quite dense. Good
+introductions can be found in \cite{Thompson1991}, \cite{Nordstrom1990},
+and \cite{Martin-Lof1984} himself.
+
+Section \ref{sec:equality} will introduce propositional equality. The
+properties of propositional equality will be discussed along with its
+limitations. After reviewing some extensions to propositional equality,
+we will explain why identifying definitional equality with propositional
+equality causes problems.
+
+Section \ref{sec:ott} will introduce observational equality, following
+closely the original exposition by \cite{Altenkirch2007}. The
+presentation is free-standing but glosses over the meta-theoretic
+properties of OTT, focusing on the mechanism that make it work.
+
+Section \ref{sec:kant-theory} will describe \mykant, a system we have
+developed incorporating OTT along constructs usually present in modern
+theorem provers. Along the way, we describe these additional features
+and their advantages. Section \ref{sec:kant-practice} will describe an
+implementation implementing part of \mykant. A high level design of the
+software is given, along with a few specific implementation issues
+
+Finally, Section \ref{sec:evaluation} will asses the decisions made in
+designing and implementing \mykant, and Section \ref{sec:future-work}
+will give a roadmap to bring \mykant\ on par and beyond the
+competition.
+
+\subsection{Contribution}
+
+The goal of this thesis is threefold: