\documentclass[aspectratio=1610,xcolor={dvipsnames}]{beamer}
\usepackage[utf8]{inputenc}
\usepackage{relsize}
\usepackage{amsmath}
\usepackage{agda}
\usepackage{caption}
\usepackage{catchfilebetweentags}
\usepackage{cite}
\usepackage{fancyvrb}
\usepackage{fontspec}
\usepackage{hyperref}
\usepackage{newunicodechar}
\usepackage{setspace}
\usepackage{url}

\usetheme{Berlin}
\usecolortheme{lily}
\setbeamercovered{transparent}

\newfontfamily\PragmataPro[Extension=.ttf,NFSSFamily=PragmataPro]{PragmataPro}

\usepackage{tikz}
\usetikzlibrary{positioning}

\setstretch{1.25}
\fvset{fontfamily=PragmataPro}

\AtBeginSection[] {
  \begin{frame}
    \frametitle{\insertsectionhead}
    \tableofcontents[currentsection]
  \end{frame}
}

\titlegraphic{
  \centering
  \vspace{-1cm}
  \includegraphics[width=.2\textwidth,height=.35\textheight]{cesk.png}
}
\title{First class continuations with CEK in Agda}
\author{Michael Zhang}
\date{}

\begin{document}

\begin{frame}
  \maketitle
\end{frame}

\section{Background}

\begin{frame}
  \frametitle{Overview}

  \begin{itemize}
    \item Lambda calculus in A-normal form.
    \item CESK machine is my dynamic system.
    \item \texttt{call/cc} is my extra feature.
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{What is a CESK machine?}

  \begin{itemize}
    \item Abstract machine for interpreters, introduced by Matthias Felleisen.
    \item Stands for $C$ontrol, $E$nvironment, $S$tore, $K$ontinuation.
    \item Based on Matt Might's blog post on CESK machines.
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{What do C, E, S, and K mean?}

  \begin{itemize}
    \item $C$ontrol is your current term.
    \item $E$nvironment is a list of addresses.
    \item $S$tore is a mapping of addresses to values.
    \item $K$ont is what gets evaluated next.
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Why continuations?}

  \begin{itemize}
    \item Useful for implementing other language constructs
      \begin{itemize}
        \item call/cc
        \item Exceptions
        \item Mutation
        \item Recursion
      \end{itemize}
  \end{itemize}
  
  \begin{exampleblock}{Example}
    $\color{Plum}4 + \color{black}(\texttt{call/cc} \color{Orange}(\lambda k .\:k\:2)\color{black}) \Rightarrow
     \color{Orange}(\lambda k.\:k\:2)\color{black} (\lambda n.\:\color{Plum}4 + \color{black}n) \Rightarrow
     6$
  \end{exampleblock}
\end{frame}

\begin{frame}
  \frametitle{A-Normal Form}

  \begin{itemize}
    \item Separates atomic expressions from state-mutating ones
    \item Atomic expressions evaluate to values
    \item This approach cleans up the implementation a bit
  \end{itemize}
\end{frame}

\section{Agda Implementation}

\begin{frame}[fragile]
  \frametitle{Keeping track of types}

  \begin{Verbatim}[fontsize=\relsize{-3}]
    data Aexp (Tω : Type) Context : Type → Set
    data Exp (Tω : Type) Context : Type → Set

    data Aexp Tω Γ where
      value : ∀ {A} → Value Tω A → Aexp Tω Γ A
      zero : Aexp Tω Γ `ℕ
      suc : Aexp Tω Γ `ℕ → Aexp Tω Γ `ℕ
      `_ : ∀ {A} → Γ ∋ A → Aexp Tω Γ A
      ƛ : ∀ {A B : Type} → Exp Tω (Γ , A) B → Aexp Tω Γ (A ⇒ B)

    data Exp Tω Γ where
      atomic : ∀ {A} → Aexp Tω Γ A → Exp Tω Γ A
      case : ∀ {A} → Aexp Tω Γ `ℕ → Exp Tω Γ A → Aexp Tω Γ (`ℕ ⇒ A) → Exp Tω Γ A
      _·_ : ∀ {A B} → Aexp Tω Γ (A ⇒ B) → Aexp Tω Γ A → Exp Tω Γ B
      abort : ∀ {A} → Aexp Tω Γ ⊥ → Exp Tω Γ A
      _∘_ : ∀ {A} → Aexp Tω Γ K[ A ⇒ ⊥ ] → Aexp Tω Γ A → Exp Tω Γ ⊥
      call/cc : ∀ {A} → Aexp Tω Γ (K[ A ⇒ ⊥ ] ⇒ Tω) → Exp Tω Γ A
  \end{Verbatim}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Progress and Preservation}

  \begin{itemize}
    \item We get preservation for free.
    \item Closed step function gives us progress.
  \end{itemize}

  \vspace{.5cm}

  \begin{Verbatim}[fontsize=\relsize{-2}]
    data StepResult (A : Type) : Set where
      part : State A → StepResult A
      done : Value A A → StepResult A
    step : ∀ {Tω : Type} → State Tω → StepResult Tω
  \end{Verbatim}
\end{frame}

\begin{frame}[fragile]
  \frametitle{Evaluation}

  \begin{Verbatim}[fontsize=\relsize{-2}]
    data EvalResult : Set where
      complete : ∀ {A} → StepResult A → EvalResult
      exhausted : ∀ {A} → State A → EvalResult

    eval′ : ∀ {A} → ℕ → State A → EvalResult
    eval′ 0 s = exhausted s
    eval′ (suc n) s with step s
    ... | part x = eval′ n x
    ... | done x = complete $ done x

    eval : ∀ {A} → ℕ → Exp A ∅ A → EvalResult
    eval n e = eval′ n (inject e)
  \end{Verbatim}
\end{frame}

\section{Conclusion}

\begin{frame}
  \frametitle{Links}

  \begin{itemize}
    \item Source code of this project \url{https://git.sr.ht/~mzhang/agda-project}
    \item Matt Might's blog \url{https://matt.might.net/articles/cesk-machines}
  \end{itemize}
\end{frame}

\end{document}

% vim: set sw=2 :