\section{Conclusions}

    \begin{frame}
        %% João Pizani wants to present this :)
        \frametitle{Achieved}

        \begin{itemize}
            \item Agda ``framework'' for deriving compiler correctness proofs
            \begin{itemize}
                \item Compilers with \textbf{typed source} and \textbf{typed target}
                \item Given correctness of a ``naïve'' compiler, derive correctness of ``optimized'' version
            \end{itemize}

           \item Correctness proof for an expression language (with sequencing)
           \begin{itemize}
               \item As ``instance'' of this framework
           \end{itemize}
        \end{itemize}
    \end{frame}

    \begin{frame}
        % Wout presents this, right? :)
        \frametitle{Agda limitations we faced}

        \begin{itemize}
            \item Strict positivity requirement
            \begin{itemize}
                \item When defining fixed point type operators
            \end{itemize}

            \item Totality checker
            \begin{itemize}
                \item When defining folds
            \end{itemize}

            \item Type checking with positivity check disabled made debugging hard
            \begin{itemize}
                \item Stack overflow, memory consumption
            \end{itemize}
        \end{itemize}
    \end{frame}
             
    \begin{frame}
        \frametitle{Yet to be done}

        \begin{itemize}
            % João here :)
            \item Sequence clause of ``basic'' (non-lifted) correctness proof

            % Wout here :)
            \item Prove a final lemma to complete the lifting (fusion law)
        \end{itemize}
    \end{frame}

