\documentclass[a4paper]{article}

%% Standard packages
\usepackage{times}
\usepackage{a4}
\usepackage{graphicx}
\usepackage{mathtools}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{hyperref}
\usepackage{color}

%% Unicode support
\usepackage[utf8x]{inputenc}
\usepackage{ucs}


%% Agda
\usepackage{agda/agda}
\usepackage{catchfilebetweentags}


%% PDF metainformation
\usepackage{datetime}
\usepackage{ifpdf}
\ifpdf
\pdfinfo{
    /Author (Joao Paulo Pizani Flor, Wout Elsinghorst)
    /Title (Proving Compiler Correctness with Dependent Types)
    /Keywords (Agda, Dependently-typed programming, Compiler correctness, typed bytecode)
    /CreationDate (D:\pdfdate)
}
\fi


%% LaTeX meta-information
\title{Proving Compiler Correctness with Dependent Types}

\date{\today}
\author {
    João Paulo Pizani Flor \texttt{<j.p.pizaniflor@students.uu.nl>} \\
    \and Wout Elsinghorst \texttt{<w.l.elsinghorst@students.uu.nl>} \\
}

\newcommand{\fref}[1]{\emph{Figure} \ref{lst:#1}}


%% The document itself
\begin{document}
    \maketitle

    \section{Introduction}
    \label{sec:intro}
        In this report we describe our work for the final project of the master course
        "Theory of Programming and Types" at Utrecht University. Our research involves
        the question of compiler correctness, i.e, giving a \emph{specification} for
        a language (a semantics), and proving that a compiler for that language respects
        the given semantics.

        Concretely, our notion of correctness depends on two semantics, respectively for the source
        and object languages of the compiler. We define a denotational semantics (\texttt{eval}) for the source
        language, as well as an operational semantics (\texttt{exec}) for the target machine. Correctness
        states that evaluation is equal to compilation composed with execution.

        More specifically, we were interested in having \emph{machine-checked} proofs of correctness,
        i.e, proofs written in the language of an interactive proof assistant. Some initiatives in
        this direction are already being taken, most famously CompCert, a formally verified compiler
        for the C language, which had its proof written in the \emph{Coq} proof assistant.

        %Comparing our work to ComCert seems a bit pretentious?
        
        %TODO: rewrite this, remove pretentiousness, keep relevant information
        %Our work (definitions and proofs) is, on the other hand, written in the
        %\emph{Agda} programming language instead of emph{Coq} It also also differs from CompCert
        %in that we use dependent types to make source and object languages (as well as the compiler)
        %have some meta-theoretical properties (for example, type preservation) \emph{by construction},
        %instead of proving them separately.

        Dependent types allow us to embed, as indices to the language definitions and in the type
        of the ``compile'' function, constraints which make these definitions correct.

        The rest of the report is organized as follows: on section \ref{sec:goals} we present the
        related papers which served as the basis for our research, and state precisely which were
        our contributions. In section \ref{sec:basic} we present the definitions for our 
        \emph{source} and \emph{object} languages and give the implementation of the compiler itself.
        In section \ref{sec:correctness} we define a notion of compiler correctness and prove that our compiler
        is correct according to this definition. Section \emph{sec:lifting} introduces a smarter version of 
        the object language, in which sharing is captured, together with a compiler which
        produces code in this new language. We then proceed to describe how, given a correctness proof for a 
        ``naïve'' compiler, a proof of correctness for the smarter version can be obtained.

        \textbf{Acknowledgments:} We are pleased to thank Wouter Swierstra for his help and valuable insights.
        
    \section{Related work/Goals}
    \label{sec:goals}
        % Mention two papers we based our work on
        On researching the topic of compiler correctness in the context of dependent types, we first encountered
        the paper ``A type-correct, stack-safe, provably correct expression compiler in Epigram'' \cite{typed-stack-safe-compiler}.
        In this paper, a \emph{very simple} (but \emph{typed}) expression language is presented,
        along with a \emph{typed bytecode} definition. The correctness of this compiler is then formulated and proven.
        
        Both language definitions, the semantics for each of them, the compiler and its correctness proof
        were all written in Epigram, a dependently-typed programming language. Therefore,
        even though the authors admit that the paper carries no real novelty value related to compiler
        construction, we still felt this paper could serve well as the ``basis'' for our project, as they
        treat compilation of \emph{typed source} to \emph{typed bytecode}, and also use a dependently-typed
        implementation language.

        So our work started with trying to extend the source language from \cite{typed-stack-safe-compiler},
        and add constructs to it that made it more powerful. Then we came across the paper
        ``Proving Correctness of Compilers using Structured Graphs''\cite{compiler-correctness-structured-graphs}.
        In this paper, the author discusses the issue of \emph{sharing} of bytecode, that is, that
        some high-level language constructs (typically control flow related constructs,
        such as exception handling of conditional branching) map into low-level code which has
        \emph{shared blocks of code among different execution paths}.

        One way to compile these control flow constructs would be to extend the bytecode language with
        explicit jumps and labels, a solution which is often taken in ``real-world'' compilers,
        but which makes analyzing bytecode and proving compiler correctness much more complex.
        A simpler way to handle these situations is to just \emph{replicate} the shared code when
        compiling constructs which generate different execution paths.

        A compiler which works by using a jump-and-label-free bytecode and replicates shared code
        is easier to analyze, but the practically desirable behaviour is, off course, to represent
        the sharing. The main contribution of \cite{compiler-correctness-structured-graphs} is a
        systematic way in which a proof of correctness for a ``naïve'' (code-duplicating) compiler can
        be used to construct the correctness proof for a ``sharing optimized'' version of that compiler;
        a rather elegant approach.

        % Our wish to join the contributions of both papers
        The overall goal of our project was, therefore, to integrate the solutions given both in
        \cite{typed-stack-safe-compiler} and \cite{compiler-correctness-structured-graphs}.
        To achieve this goal we needed to make some adjustments to the definitions and proofs of
        the reference papers. These adjustments are what we perceive as our main contributions
        with this project:

        % What adaptations we did to each approach to help them work together:
        \begin{itemize}
            \item The solution in \cite{compiler-correctness-structured-graphs}
                used Haskell as implementation language (along with some proofs given in Coq).
                \begin{itemize}
                    \item We needed, therefore, to adapt definitions such as fixed point operators and generic
                        maps/folds to the \emph{total} setting of Agda.
                \end{itemize}

            % Make functors and proofs of the lifting approach indexed
            \item The example bytecode language used in \cite{compiler-correctness-structured-graphs}
                to illustrate the method is \emph{untyped}.
                \begin{itemize}
                    \item To make the proof derivation scheme work for \emph{typed} bytecode,
                        we needed to also adapt most of the generic data structures presented to become \emph{indexed}.
                \end{itemize}

            % Extension in the Src to reveal "sharing opportunities"
            \item The example control flow construct used in \cite{compiler-correctness-structured-graphs}
                to introduce sharing (exceptions) was also not immediately applicable to being
                modeled in a total setting.
                \begin{itemize}
                    \item Specifically, the way in which it was implemented (by using Higher-Order Abstract Syntax)
                        clashed with Agda's requirement of \emph{strict positivity}\footnote{Strict positivity implies
                        that fields of a datatype can't be of function type with the respective datatype as its 
                        domain ('in negative position'). So constructors of the form $mkFoo : Foo \to \cdots \to Foo$
                        are not allowed.} Exceptions required the \texttt{Stack} datatype to contain handlers of the form 
                        $Stack \to Stack$, violating the positivity requirement.
                        
                    \item We chose a simpler sharing-inducing extension to the language of
                        \cite{typed-stack-safe-compiler} (sequencing and conditional branching).
                        This extension is explained in more detail in section \ref{sec:basic}
                \end{itemize}
        \end{itemize}
        


    \section{Source and Target Language}
    \label{sec:basic}
        % Introduce compiler correctness in general (no models mentioned)

        % Talk about our model with sequencing and the "vector values"
        Our source language (\texttt{Src}) is based upon, and therefore very similar, to the one
        defined in \cite{typed-stack-safe-compiler}. It is a typed expression language, in which
        the types are naturals and booleans. There are no binding or application constructs
        in this language, therefore no arrow type constructor. First, we show the type language for
        Src:

        \begin{figure}[h!]
            \ExecuteMetaData[agda/tex/Report.tex]{Tys}
            \caption{Types for our source language.
                \label{lst:tys}
            }
        \end{figure}

        When naming constructs of the languages which are our "object of study", we give
        subscripts to distinguish them from similarly named definitions in Agda (the \emph{metalanguage}).
        In the case of the source language, the names are subscripted by a small-case ``s''.

        \begin{figure}[h!]
            \ExecuteMetaData[agda/tex/Report.tex]{Src}
            \caption{
                The \texttt{Src} datatype definition.
                \label{lst:src}
            }
        \end{figure}

        The definition of \texttt{Src} makes clear what is the main difference between our source language
        and the used defined in \cite{typed-stack-safe-compiler}: we have an additional \textbf{sequencing}
        construct. Even though the datatype definition is increased by only one constructor,
        this change has several subtleties:

        \begin{itemize}
            \item All subexpressions in a sequence are required to be of the same base type
            \item No arithmetic or boolean operators over sequences
                \begin{itemize}
                    \item This is enforced by making expressions have a \emph{size}
                \end{itemize}
        \end{itemize}

        As important as defining the constraints on well-formed expressions is also defining
        a \emph{semantics} for \texttt{Src}. We follow the same idea as in \cite{typed-stack-safe-compiler}
        and provide a denotational semantics for \texttt{Src}, written as a function \texttt{eval}
        which maps terms of \texttt{Src} to values.

        \begin{figure}[h!]
            \ExecuteMetaData[agda/tex/Report.tex]{eval}
            \caption{Semantics for the \texttt{Src} language.
                \label{lst:eval}
            }
        \end{figure}

        Because of the sequencing construct, we chose our values to be \emph{vectors} of naturals or
        booleans. The usage of vectors as values matches the requirement we imposed that sequences
        of expressions have to be uniformly-typed. Also, the size of the vector resulting from
        evaluation matches the size of the \texttt{Src} expression.

        A last interesting remark about \texttt{eval} is that the \emph{type signature of eval
            expresses type preservation}. This phenomenon, of having proven a meta-theoretical
        property ``for free'', is allowed by the use of dependent types on the definitions of the
        language and the evaluator. On a non-dependent setting, such a property would have to be
        proven separately, in an ``offline'' proof.

        Having defined \texttt{Src} and its semantics (\texttt{eval}),
        we now move on to defining the target language (\texttt{Bytecode}) and its corresponding semantics (\texttt{exec}).
        This target language is a \emph{typed} stack bytecode, and therefore it operates on \emph{typed stacks}:

        \begin{figure}[h!]
            \ExecuteMetaData[agda/tex/Report.tex]{StackType}
            \caption{The type of a \texttt{Stack}.
                \label{lst:stacktype}
            }
        \end{figure}

        \begin{figure}[h!]
            \ExecuteMetaData[agda/tex/Report.tex]{Stack}
            \caption{Definition of a \emph{typed} stack.
                \label{lst:stack}
            }
        \end{figure}

        The \texttt{Stack} type is \emph{indexed} by \texttt{StackType}.
        The same \texttt{StackType} indices come into play in the definition of the \texttt{Bytecode} datatype:
        Each bytecode instruction performs a certain stack manipulation,
        and therefore each instruction is a value of type \texttt{Bytecode s₁ s₂},
        where \texttt{s₁} is the \emph{input StackType} and \texttt{s₂} is the \emph{output StackType}.

        %% Bytecode
        \begin{figure}[h!]
            \ExecuteMetaData[agda/tex/Report.tex]{Bytecode}
            \caption{Typed bytecode instructions.
                \label{lst:bytecode}
            }
        \end{figure}

        The semantics of the bytecode are defined in by the function \texttt{exec}, whose type 
        signature can be read (due to \emph{currying}) as mapping a value of \texttt{Bytecode}
        into a function which relates the initial pre-execution \texttt{Stack} to the final post-execution \texttt{Stack}.

        %% exec
 %       \begin{figure}[h!]
            \ExecuteMetaData[agda/tex/Report.tex]{exec}
 %           \caption{Semantics for \texttt{Bytecode}.
 %               \label{lst:exec}
 %           }
 %       \end{figure}

        
    \section{Compiler Correctness}
    \label{sec:correctness}
        With both source and target languages of our compiler in place, the compiler itself is now easily defined:

        %% compiler
 %       \begin{figure}[h!]
            \ExecuteMetaData[agda/tex/Report.tex]{compile}
 %           \caption{The ``naïve'' compiler, generating tree-like bytecode.
 %               \label{lst:compile}
 %           }
 %       \end{figure}

        Correctness of the compiler is defined as stating that \texttt{compile} should respect both evaluation and execution semantics: executing
        the code directly with the \texttt{eval} function should result in the same value as first compiling to \texttt{Bytecode} and
        then executing the \texttt{Bytecode} on an empty initial stack. Formally we need to proof the following:
        
        \ExecuteMetaData[agda/tex/Report.tex]{correct}
        
        The proof follows by induction on the source language expression.
        The value case is proven using only beta reduction (and reflexivity).
        For the cases of addition and simple conditional (no suffix) we prove correctness
        by rewriting with the induction hypothesis and matching on the operands (in the case of addition) or the condition (in the conditional case).

        The most complex case of the correctness proof is the sequencing case:
        here we use, besides the induction hypotheses over the operands, also a lemma involving prepending lists to vectors:

        \begin{figure}[h!]
\begin{verbatim}
lemmaPrepend : ∀ {m n t st}
               → (v₁ : Vec [[ t ]] m) (v₂ : Vec [[ t ]] n) (l : Stack st)
               → prepend (v₁ +++ v₂) l ≅ prepend v₁ (prepend v₂ l)
\end{verbatim}
            \caption{Prepending a concatenation equals prepending the first list then the second.
                \label{lst:lemmaprepend}
            }
        \end{figure}

        Unfortunately, this lemma doesn't get us quite as far as we would want. What's left is a seemingly-not-so-difficult proof involving heterogeneous 
        equality that doesn't lend itself to closure that easily. Although we're not really sure how to finish the proof, we've reduced it to two
        self contained holes that can be attacked independently.
        

    \section{Graph Representation}
    \label{sec:lifting_introduction}
        % What is the sharing opportunity (diamond diagram or just Src code example)
           % single Src term
           % smart and dumb bytecode generated

        % There is this different representation of Bytecode (graph) that could capture sharing...
            % Let and Var make the sharing happen...
            % Give "BytecodeG-like'' definition (two extra constructs)

        % If we make Bytecode into functor, we can have different representations by
        % applying fixed-point-like operators
          % Htree (Hfix, indexed fixed-point), HGraph (not iso really)
          
          % commutative diagram (with execT, unravel, execG)
          % preserves execution semantics, but loses sharing

        % State the "lifting" theorems (top-down):
            % Grand finale: correctG (begin with ``lifting'' module), explain parts needed
                %% Lemmas, lemma
                     %% Fusion (mention paper with simple (non-indexed) proof).

                     
        \subsection{Introduction}
        The compiler in the version currently given generates bytecode where common substructures aren't explicitly shared. A piece of code
        sequenced after an if-then-else branching statement gets copied to both the true and the false branch. This
        gives the generated code a tree like structure which (allegedly) makes it easy to reason about. Unfortunately, 
        the duplication results in exponential memory usage: for every branching statement appearing in the code, two 
        copies of the code below it must be kept in memory. The following example shows this behaviour:
        
        \ExecuteMetaData[agda/tex/Report.tex]{dupSource}
        
        The following code is generated:
        
        \ExecuteMetaData[agda/tex/Report.tex]{dupTarget}
        
        One can see that the code the expression \texttt{vₛ 5 ⟫ₛ vₛ 7} is generated twice.
        
        A solution to this problem is given in \cite{compiler-correctness-structured-graphs},
        where instead of as a tree, the bytecode is now represented as an acyclic graph. In this representation, structures
        can be given names which can be used to refer to the substructure. Only one copy of the structure is kept in memory, 
        independent of the number of times this structure is referred to. This more efficient representation
        is nice if performance is a concern, but it arguably makes to harder to reason about. Ideally, one would like to 
        write proofs using the tree represenation while making use of the graph representation when actually using the compiler. 
        Luckily, \cite{compiler-correctness-structured-graphs} also describes how correctness proofs from the tree repesentation 
        can be transferred ('lifted') to the graph representation. To make this lifting machinery work we first have to make the 
        tree structure explicit.
                     
        
        \subsection{Explicit Tree Structure}
        
        An explicit tree description of the \texttt{Bytecode} datatype is obtained by representing it as the fixed point of 
        some functor. This makes the recursive positions explicit and will later allow us to label them. Because \texttt{Bytecode} 
        is an \emph{indexed} datatype, we represent it using an \emph{indexed} functor. Fixed points of indexed functors are obtained 
        by instantiating them using the following datatype:
        
        
        \ExecuteMetaData[agda/tex/Report.tex]{HTree}
        
        One should notice that that this datatype doesn't actually meet the no-positivity requirement \ref{sec:goals}. We've locally disabled the 
        no-positivity check as to allow us to continue work in this direction. We reasoned that instantiating \texttt{HTree} with a stricly 
        positive functor would not allow any inconsistencies to leak out of the module. Unfortunately, disabling this check resulted in a number
        of compiler bugs (or maybe expected behaviour? we don't know) which resulted in stack overflows when querying types and memory exhaustion
        compiling certain functions. The compromises that had to be made to work around these problems will be addressed in the end of this section.
        
        Using \texttt{HTree}, one can use the following functor
        
        \ExecuteMetaData[agda/tex/Report.tex]{BytecodeF}
 
        to obtain an datatype isomorphic to the original: \texttt{∀ s s' . Bytecode s s' ~ HTree BytecodeF s s'}
        
        The isomorphism is witnessed by the following two functions:
        
        \ExecuteMetaData[agda/tex/Report.tex]{isoToTree}
        \ExecuteMetaData[agda/tex/Report.tex]{isoFromTree}
        
        The functions \texttt{compile} and \texttt{exec} have counterparts defined on this fixed point representation 
        which are called \texttt{compileT} and \texttt{execT} respectively. Correctness for the tree representation can now be stated as follows:
        
        \ExecuteMetaData[agda/tex/Report.tex]{correctT}
        
        
        One final word about trees: by defining trees we had to disable the positivity check. This resulted in bugs in agda that were triggered 
        whenever a proof involved the fold function that accompanies \texttt{HTree}. To workout these issues, we had to omit the implementation of fold
        and postulate the relevant properties so that the typechecker would never actually have to inspect the \texttt{HTree} datatype. Proving things using
        these postulates is straightforward, albeit cumbersome.  
        
        \subsection{Graph Structure}
        
        Our goal now is to define a graph structure which allows for automatic lifting of proofs from the tree structure. In the end we'd like a proof lifting
        function so that the correctness proof for graphs can be obtained as
        \begin{verbatim}
correctG = lift correctT
        \end{verbatim}
        
        Let us first start with the basics. A graph representation is obtained by the following modification of the \texttt{HTree} datatype:
        
        \ExecuteMetaData[agda/tex/Report.tex]{HGraph'}
        
        In addition to constructors representing the recursive positions, there are two constructors for representing and using shared substructures.
        The \texttt{HGraphLet} constructor is used to give tag a given substructure, which can then be referred to by the \texttt{HGraphVar} constructor. 
        
        The observant reader will notice that the indices of the \texttt{HGraphLet} constructor aren't scoped correctly. This is a minor oversight which we only
        found out about last minute. 
        
        Bytecodes which use shared substructures can now be represented as values of the type \texttt{HGraph BytecodeF}. Every \texttt{HTree BytecodeF} 
        can trivially be embedded in \texttt{HGraph BytecodeF} by ignoring the extra constructors. For graphs there are of course also the
        \texttt{execG} and \texttt{compileG} functions which define how to execute graph bytecode or compile to graph bytecode, respectively. Converting in the other direction however loses sharing
        information. Executing either the \texttt{unravel}ed graph or the original will still gave the same result. 
        
        Unfortunately, at this moment the previous example which was used to show code duplication cannot be rewritten in the more efficient graph 
        representation because the graph representation has some of it's indices mixed up.
        
        Correctness for graphs amounts to the following statement:
        
        \ExecuteMetaData[agda/tex/Report.tex]{correctG}
        
        To prove this, we provide a framework which is generic over the base functor chosen, which in our case is \texttt{BytecodeF}. 
        
        \subsection{Lifting Proofs}
        
        
        We've implemented a module called 'Lifting' which is parametrised by a correctness proof for trees and a proof that relates \texttt{compileG} 
        to \texttt{compileT} via the \texttt{unravel} function. Concretely, to obtain a proof for \texttt{correctG}, one needs to open the module 
        \texttt{Lifting} and supply it with \texttt{correctT} and following (only non-trivial) additional parameter:
        
        \ExecuteMetaData[agda/tex/Report.tex]{unravelLemma}
        
        The implementation of the \texttt{Lifting} module itself uses a generalization of the \texttt{Shortcut Fusion Theorem} which is mentioned but not proven in \cite{compiler-correctness-structured-graphs}.
        The generalization, although not in contradiction with our intuition, is not proven, and is thus one of the weak spots of our system.
        
        To actually instantiate the \texttt{Lifting} module, one needs to supply a proof of the \texttt{unravelLemma} tailored for the specific functor at hand. 
        Unfortunately, we didn't manage to supply a full proof of this lemma for our \texttt{BytecodeF} functor. There is only tiny hole left open, but 
        unfortunately this hole asks us to construct an infinite type. The requested value must have type:
        \begin{verbatim}
BytecodeF (HTree BytecodeF) ixp ixq → HTree BytecodeF ixp ix
        \end{verbatim}
        
        The \texttt{HTreeIn} constructor has this type:
        
        \begin{verbatim}
HTreeIn : ∀ {F} → F (HTree F) ixp ixq → HTree F ixp ix
        \end{verbatim}
        
        But unfortunately we're not allowed to use it. The problem seems to be that normally such an infinite type cannot escape a datatype declaration: 
        it is only allowed on the right hand side the declaration. Somehow, due to the our way of approaching the proof, this has leaked to the outside world.
        We think it is possible that a different approach would avoid exposing this type and thus allow for a full proof of this lemma.

    \section{Conclusions}
    \label{sec:conclusions}
        % Summarize contributions
        In this project, we developed a provably correct expression compiler using dependent types in the Agda programming language.
        Also, we implemented a \emph{systematic transformation} that, given the correctness proof for
        a ``basic'' compiler, can produce the correctness proof for a compiler based on the first but
        generating ``optimized'' (sharing-preserving) target code.

        We believe that, even with such small languages as the ones we chose as examples,
        this methodology of systematically ``extending'' correctness proofs when adding compiler optimizations
        is an important area of research, and that using proof assistants based on dependent types is a
        promising approach.

        % Points where we got stuck (holes, postulates)
        To conclude the report, we would like to explain what are the points in which we do not consider our work
        to be finished. These are lemmas which we believe are true, but due to some technicality or sheer
        time limitations we were not able to prove completely:

        \begin{enumerate}
            \item The sequence clause (\texttt{\_⟫\_} constructor) of the basic (non-optimized) compiler
                is depending on a lemma that was left still to be proven.
                \begin{itemize}
                    \item This lemma (\texttt{lemmaPrepend}) involves vector concatenation and a ``prepending'' operation,
                        but can only be stated (apparently) using heterogeneous equality, which hindered our attempts.
                \end{itemize}
                
            \item Whether the \emph{Shortcut Fusion Law} for folds also holds over \emph{indexed functors} is still a topic for further research. It
                  is very plausible for this law to be true, but there is no proof, and any proof would most certainly be non-trivial. It is a very large
                  gap in our framework which needs our first attention should this project be continued further.
                % What uses it, why is it used/where?
                % TODO: Wout, plz use your knowledge and expand this a bit :). <-- Knowledge used. :)

            \item The remaining part of the proof of the \emph{Unravel Lemma} probably needs a different appoach. We don't think this will pose a serious
                  problem.
            \item \texttt{HGraph} still needs some generalization to allow for more general (read: non-useless) let bindings. At the moment they are not
                  sufficient to allow us to implement the provided examples in their efficient graph form. This is a minor oversight which should require only
                  a few (but technical) local changes to fix.
        \end{enumerate}

        Finally, we would like to comment on some of the main difficulties we ran into during the
        development of this project. First of all, as already mentioned, we had to model in Agda concepts which
        do not fit easily the total setting, such as type-level fixpoint operators (violate the
        \emph{strict positivity} requirement of Agda) and generic folds over functors (which do not pass
        the totality checker). To be able to use these definitions we had to enable compilation flags and pragmas
        which made programming in Agda less ``secure''. Enabling these flags exposed some agda bugs/expected behaviour which made our 
        development experience less than pleasant. We had stack overflows when querying holes for their type and memory exhaustion when compiling
        programs. Pinpointing these problems and working around them took quite a bit of our time and we hope that future versions of agda will be
        more accommodating.


    \bibliographystyle{plain}
    \bibliography{../references}

\end{document}
