More updates to presentation

PragmataPro.ttf

@@ -0,0 +1 @@
+/home/michael/.local/share/fonts/PragmataPro_Mono_R_liga_0829.ttf

agda-project.agda-lib

@@ -1,3 +1,3 @@
-name: csci8980-project
+name: agda-project
 depend: standard-library
 include: ./src

main.tex

@@ -1,93 +1,190 @@
-\documentclass{beamer}
+\documentclass[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{CambridgeUS}
+\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 machines in Agda}
+\title{First class continuations with CEK in Agda}
 \author{Michael Zhang}
 \date{}
 
 \begin{document}
 
-% \frame{\titlepage}
-\begin{frame}[t]\vspace{1cm}
+\begin{frame}
   \maketitle
 \end{frame}
 
-\section{Primer on CESK}
+\section{Background}
 
 \begin{frame}
   \frametitle{What is a CESK machine?}
 
-  \begin{itemize}[<+->]
+  \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 \cite{might-cesk}.
+    \item Based on Matt Might's blog post on CESK machines.
   \end{itemize}
 \end{frame}
 
 \begin{frame}
-  \frametitle{What are each of the components?}
+  \frametitle{What do C, E, S, and K mean?}
 
-  \begin{itemize}[<+->]
+  \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}
+
+  \vspace{.5cm}
+
+  Example on next slide.
 \end{frame}
 
 \begin{frame}
-  \frametitle{What are continuations?}
+  \begin{exampleblock}{Example}
+    \begin{equation*} \begin{split}
+      \{ C = (\lambda .\:`0 + 2) \cdot 4, E = [], K = [halt] \} \\
+      \{ C = (\lambda .\:`0 + 2), E = [4], K = [\lambda .\:`0 \cdot 4, halt] \} \\
+    \end{split} \end{equation*}
+  \end{exampleblock}
 \end{frame}
 
 \begin{frame}
-  \begin{tikzpicture}[
-      roundnode/.style={circle, draw=green!60, fill=green!5, very thick, minimum size=7mm},
-      squarednode/.style={rectangle, draw=red!60, fill=red!5, very thick, minimum size=5mm},
-    ]
-    \node[draw, align=left, squarednode](ceskState){
-      C = $\lambda x . (\lambda y . x + y)$ \\
-      $E$ = [] \\
-      $\kappa$ = halt
-    };
-    \node[squarednode](ceskState2)[right=of ceskState]{CEK};
+  \frametitle{Why continuations?}
 
-    %lines
-    \draw[->] (ceskState.east) -- (ceskState2.west);
-  \end{tikzpicture}
+  \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}
 
-\section{Implementation}
-
 \begin{frame}
-  \frametitle{Hellosu}
+  \frametitle{A-Normal Form}
 
-  \include{./gentex/Project/Cesk.tex}
+  \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{Resources}
-  \bibliography{res}{}
-  \bibliographystyle{plain}
+  \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}

res.bib

@@ -1,21 +0,0 @@
-@phdthesis{
-  felleisen-cesk,
-  author = "Matthias Felleisen",
-  howpublished = {\url{https://www2.ccs.neu.edu/racket/pubs/dissertation-felleisen.pdf}},
-}
-
-@misc{
-  might-cesk,
-  author = "Matt Might",
-  title = "Writing an interpreter, CESK-style",
-  howpublished = {\url{https://matt.might.net/articles/cesk-machines}},
-}
-
-@misc{
-  source-code,
-  author = "Michael Zhang",
-  title = "First class continuations with CEK machines in Agda",
-  howpublished = {\url{https://git.sr.ht/~mzhang/csci8980-f21-project}},
-}
-
-@comment vim: set sw=2 :

src/Project/Definitions.agda

@@ -48,7 +48,7 @@ data Aexp Tω Γ where
 
   -- Functions
   `_ : ∀ {A} → Γ ∋ A → Aexp Tω Γ A
-  ƛ : ∀ {B} {A : Type} → Exp Tω (Γ , A) B → Aexp Tω Γ (A ⇒ B)
+  ƛ : ∀ {A B : Type} → Exp Tω (Γ , A) B → Aexp Tω Γ (A ⇒ B)
 
 data Exp Tω Γ where
   abort : ∀ {A} → Aexp Tω Γ ⊥ → Exp Tω Γ A