\section{Implementation (code)}

    \subsection{Basic correctness}

        \begin{frame}[fragile]
            %% João Pizani wants to present this :)
            \frametitle{Source}

            \begin{itemize}
                \item Source types:
                    \ExecuteMetaData[agda/tex/Source.tex]{tys}

                \item Source terms (snippet):
                    \ExecuteMetaData[agda/tex/Source.tex]{src}

                \item Denotational semantics (snippet):
                    \ExecuteMetaData[agda/tex/Source.tex]{eval}
            \end{itemize}
\end{frame}

        \begin{frame}[fragile]
            \frametitle{Bytecode}
            %% João Pizani wants to present this :)

            \begin{itemize}
                \item Typed stack:
                \ExecuteMetaData[agda/tex/Bytecode.tex]{stacktype}
                \ExecuteMetaData[agda/tex/Bytecode.tex]{stack}

                \item Typed bytecode (snippet):
                \ExecuteMetaData[agda/tex/Bytecode.tex]{bytecode}
            \end{itemize}
\end{frame}

        \begin{frame}[fragile]
            \frametitle{Compiler correctness}
            %% João Pizani wants to present this :)
            \ExecuteMetaData[agda/tex/Bytecode.tex]{compile}

            \begin{verbatim}
correct : {t : Tyₛ} {z : Sizeₛ} (e : Src t z)
        → exec (compile e) ≡ ⟦ e ⟧
            \end{verbatim}
\end{frame}


    \subsection{Lifting to sharing setting}

        \begin{frame}[fragile]
            %% Wout presents this? :)
            \frametitle{Tree fixpoints}

            \begin{itemize}
                \item Fixed Point for standard Functors
                    \ExecuteMetaData[agda/tex/Bytecode.tex]{Tree}
            
                \item Fixed Point for indexed Functors
                    \ExecuteMetaData[agda/tex/Bytecode.tex]{HTree}
            \end{itemize}
\end{frame}

        \begin{frame}[fragile]
            %% Wout presents this? :)
            \frametitle{Bytecode Tree Representation}

            \ExecuteMetaData[agda/tex/Bytecode.tex]{bytecode}
            \ExecuteMetaData[agda/tex/Bytecode.tex]{bytecodeF}

            \begin{itemize} 
                \item \texttt{Bytecode} is isomorphic to \texttt{HTree BytecodeF}
                    \begin{itemize}
                        \item \texttt{fromTree ∘ toTree ≡ id}
                        \item \texttt{toTree ∘ fromTree ≡ id}
                    \end{itemize}
            \end{itemize}
\end{frame}
                
        \begin{frame}[fragile]
            %% Wout presents this? :)
            \frametitle{Correctness on Trees}

            \ExecuteMetaData[agda/tex/Bytecode.tex]{compileT}
            \ExecuteMetaData[agda/tex/Bytecode.tex]{execT}

            \begin{verbatim}
correctT : ∀ {t z s'} → (e : Src t z) 
         → execT (compileT e) ≡ ⟦ e ⟧
            \end{verbatim}

            \begin{itemize}
                \item Proof of \texttt{correctT} can be derived from \texttt{correct}
                    \begin{itemize}
                        \item Because `Bytecode` is structurally the same as `HTree BytecodeF`
                    \end{itemize}
            \end{itemize}
\end{frame}

        \begin{frame}[fragile]
            \frametitle{Graphs}
            %% Wout presents this? :)
            % Sample code from page 9, showing let/var

            \begin{verbatim}
data HGraph .. : ... -> Set where ...
            \end{verbatim}
            
            \begin{itemize}
                \item \texttt{HGraph} is similar (``includes'') \texttt{HTree}
                \begin{itemize}
                    \item But with extra constructors to represent \emph{shared subgraphs}
                \end{itemize}
            
                \item \texttt{Bytecode} is not \emph{exactly} isomorphic to \texttt{HGraph BytecodeF}:
                \begin{itemize}
                    \item We have: \texttt{fromGraph ∘ toGraph ≡ id}
                    \item But: \texttt{toGraph ∘ fromGraph ≠ id}
                    \item \texttt{HGraph → Bytecode → HGraph} loses sharing
                \end{itemize}
            \end{itemize}
\end{frame}
         
         \begin{frame}[fragile]
            %% Wout presents this? :)
            \frametitle{Bytecode Graph Representation}

            \ExecuteMetaData[agda/tex/Bytecode.tex]{compileG}
            \ExecuteMetaData[agda/tex/Bytecode.tex]{execG}

            \begin{verbatim}
correctG : ∀ {t z} → (e : Src t z) 
         → execG (compileG e) ≡ ⟦ e ⟧
            \end{verbatim}
            
            \begin{itemize}
                \item Using machinery, we get this proof derived from \texttt{correct}
            \end{itemize}
\end{frame}

