X-Git-Url: https://git.enpas.org/?a=blobdiff_plain;f=presentation.tex;h=2184ae49c31d3e0d65748257619744bf7538f3c5;hb=HEAD;hp=3492be8bd935d25eb46d0e7f3a3cc296fb103fcd;hpb=d126310824d9f10af2ef1eb4e21a65026abd97e1;p=bitonic-mengthesis.git

diff --git a/presentation.tex b/presentation.tex
index 3492be8..2184ae4 100644
--- a/presentation.tex
+++ b/presentation.tex
@@ -12,6 +12,13 @@
 
 \usepackage{centernot}
 \usepackage{cancel}
+\usepackage{tikz}
+\usetikzlibrary{shapes,arrows,positioning}
+\usetikzlibrary{intersections}
+\pgfdeclarelayer{background}
+\pgfdeclarelayer{foreground}
+\pgfsetlayers{background,main,foreground}
+
 
 \setlength{\parindent}{0pt}
 \setlength{\parskip}{6pt plus 2pt minus 1pt}
@@ -228,14 +235,14 @@
 \begin{frame}
   \frametitle{\mykant?}
 
-  \mykant\ is an \emph{interactive theorem prover}, implemented in
-  Haskell.
+  \mykant\ is an \emph{interactive theorem prover}/\emph{functional
+    programming language}, implemented in Haskell.
 
-  It is similar in scope to Agda or Coq, but with a more powerful notion
-  of \emph{equality}.
+  It is in the tradition of Agda and Epigram (and to a lesser extent
+  Coq), but with a more powerful notion of \emph{equality}.
 
-  We figured out its theory, but do not have a complete
-  implementation---although most of the work is done.
+  We have figured out theory of \mykant, and have a near-complete
+  implementation.
 \end{frame}
 
 \begin{frame}
@@ -280,67 +287,68 @@
 \end{frame}
 
 \begin{frame}
-  \frametitle{Theorem provers, dependent types} First class types: we
-  can return them, have them as arguments, etc.
+  \frametitle{Theorem provers, dependent types}
+  \begin{center}
+    \Huge
+    types $\leftrightarrow$ propositions
+
+    programs $\leftrightarrow$ proofs
+  \end{center}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Theorem provers, dependent types}
   \[
-  \begin{array}{@{}l@{\ }l@{\ \ \ }l}
-    \mysyn{data}\ \myempty & & \text{No members.} \\
-    \mysyn{data}\ \myunit  & = \mytt & \text{One member.} \\
-    \mysyn{data}\ \mynat   & = \mydc{zero} \mydcsep \mydc{suc}\myappsp\mynat & \text{Natural numbers.}
+  \begin{array}{@{}l@{\ \ \ }l}
+    \mysyn{data}\ \myempty & \text{No members.} \\
+    \mysyn{data}\ \myunit \mapsto \mytt & \text{One member.}
   \end{array}
   \]
-  $\myempty : \mytyp$, $\myunit : \mytyp$, $\mynat : \mytyp$.
 
   $\myunit$ is trivially inhabitable: it corresponds to $\top$ in
   logic.
-
+  \[
+  \mytt : \myunit
+  \]
   $\myempty$ is \emph{not} inhabitable: it corresponds to $\bot$.
   \[
   \myfun{absurd} : \myempty \myarr \myb{A}
   \]
+
+  First class types: we can return them, have them as arguments, etc:
+  $\myempty : \mytyp$, $\myunit : \mytyp$.
 \end{frame}
 
 \begin{frame}
   \frametitle{Theorem provers, dependent types}
-  % TODO examples first
-
-  We can express relations:
+  \[ \mysyn{data}\ \mylist{\myb{A}} \mapsto \mynil \mydcsep \myb{A} \mycons \mylist{\myb{A}} \]
+  We want to express a `non-emptiness' property for lists:
   \[
   \begin{array}{@{}l}
-    (\myfun{${>}$}) : \mynat \myarr \mynat \myarr \mytyp \\
-    \begin{array}{@{}c@{\,}c@{\,}c@{\ }l}
-      \mydc{zero} & \mathrel{\myfun{$>$}} & \myb{m} & = \myempty \\
-      \myb{n}     & \mathrel{\myfun{$>$}} & \mydc{zero} & = \myunit \\
-      (\mydc{suc} \myappsp \myb{n}) & \mathrel{\myfun{$>$}} & (\mydc{suc} \myappsp \myb{m}) & = \myb{n} \mathrel{\myfun{$>$}} \myb{m}
+    \myfun{non-empty} : \mylist{\myb{A}} \myarr \mytyp \\
+    \begin{array}{@{}l@{\myappsp}c@{\ }l}    
+    \myfun{non-empty} & \mynil & \mapsto \myempty \\
+    \myfun{non-empty} & (\myb{x} \mycons \myb{l}) & \mapsto \myunit
     \end{array}
   \end{array}
   \]
 
-  A term of type $\myb{m} \mathrel{\myfun{$>$}} \myb{n}$ represents a
-  \emph{proof} that $\myb{m}$ is indeed greater than $\myb{n}$.
+  A term of type $\myfun{non-empty} \myappsp \myb{l}$ represents a
+  \emph{proof} that $\myb{l}$ is indeed not empty.
   \[
-  \begin{array}{@{}l}
-    3 \mathrel{\myfun{$>$}} 1 \myred \myunit \\
-    2 \mathrel{\myfun{$>$}} 2 \myred \myempty \\
-    0 \mathrel{\myfun{$>$}} \myb{m} \myred \myempty
+  \begin{array}{@{}l@{\ \ \ }l}
+    \text{Can't prove} & \myfun{non-empty}\myappsp \mynil \myred \myempty \\
+    \text{Trivial to prove}  & \myfun{non-empty}\myappsp(2 \mycons \mynil) \myred \myunit
   \end{array}
   \]
 \end{frame}
 
 \begin{frame}
   \frametitle{Example: safe $\myfun{head}$ function}
-
+  \only<3>{We can eliminate the `empty list' case:}
   \[
   \begin{array}{@{}l}
-    \mysyn{data}\ \mylist{\myb{A}} = \mynil \mydcsep \myb{A} \mycons \mylist{\myb{A}} \\
-    \ \\
-    \myfun{length} : \mylistt{\myb{A}} \myarr \mynat \\
-    \begin{array}{@{}l@{\myappsp}c@{\ }c@{\ }l}
-      \myfun{length} & \mynil & \mapsto & \mydc{zero} \\
-      \myfun{length} & (\myb{x} \mycons \myb{xs}) & \mapsto & \mydc{suc} \myappsp (\myfun{length} \myappsp \myb{xs})
-    \end{array} \\
-    \ \\
-    \myfun{head} : \myfora{\myb{l}}{\mytyc{List}\myappsp\myb{A}}{ \myfun{length}\myappsp\myb{l} \mathrel{\myfun{$>$}} 0 \myarr \myb{A}} \\
+    \myfun{head} : \myfora{\myb{l}}{\mytyc{List}\myappsp\myb{A}}{ \myfun{non-empty}\myappsp\myb{l} \myarr \myb{A}} \\
     \begin{array}{@{}l@{\myappsp}c@{\myappsp}c@{\ }c@{\ }l}
       \myfun{head} & \mynil & \myb{p} & \mapsto & \only<1,2>{\myhole{?}}\only<3>{\myabsurd\myappsp\myb{p}} \\
       \myfun{head} & (\myb{x} \mycons \myb{xs}) & \myb{p} & \mapsto & \myb{x}
@@ -351,83 +359,76 @@
   \only<1>{
     The logic equivalent would be
     \[
-    \forall \myb{l} {:} \mylist{\myb{A}}.\ \myfun{length}\myappsp\myb{l} \mathrel{\myfun{$>$}} 0 \myarr \myb{A}
+    \forall \myb{l} {:} \mylist{\myb{A}}.\ \myfun{non-empty}\myappsp\myb{l} \myarr \myb{A}
     \]
     `For all non-empty lists of type $\myb{A}$, we can get an element of $\myb{A}$.'
   }
   \only<2>{
   The type of $\myb{p}$ in the $\myhole{?}$ is $\myempty$, since
-  \[\myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 \myred 0 \mathrel{\myfun{$>$}} 0 \myred \myempty \]}
+  \[\myfun{non-empty}\myappsp\mynil \myred \myempty \]}
+  \only<3>{
+    Remember:
+    \[ \myfun{absurd} : \myempty \myarr \myb{A} \]
+  }
 \end{frame}
 
 \begin{frame}
   \frametitle{How do we type check this thing?}
+  \[\text{Is\ } \myfun{non-empty}\myappsp(3 \mycons \mynil) \text{\ the same as\ } \myunit\text{?}\]
+  Or in other words, is
+  \[ \mytt : \myunit \]
+  A valid argument to
   \[
-  \myfun{head} \myappsp \mylistt{3} : \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \myarr \mynat
-  \]
-  Is it the case that
-  \[ \mytt : \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \]
-  Or
-  \[ \myfun{head} \myappsp \mylistt{3} : \myunit \myarr \mynat \]
-
-  Will $\mytt : \myunit$ do as an argument?  In other words, when type
-  checking, do we have that
-  \[
-  \begin{array}{@{}c@{\ }c@{\ }c}
-    \myunit & \mydefeq & \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \\
-    \myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 & \mydefeq & \myempty \\
-    (\myabs{\myb{x}\, \myb{y}}{\myb{y}}) \myappsp \myunit \myappsp \myappsp \mynat & \mydefeq & (\myabs{\myb{x}\, \myb{y}}{\myb{x}}) \myappsp \mynat \myappsp \myunit \\
-    & \vdots &
-  \end{array}
+  \myfun{head} \myappsp (3 \mycons \mynil) : \myfun{non-empty}\myappsp(3 \mycons \mynil) \myarr \mynat
   \]
-  ?
-\end{frame}
-
-\begin{frame}
-  \frametitle{Definitional equality}
-  
-  The type checker needs a notion of equality between types.
 
-  We reduce terms `as far as possible' (to their \emph{normal form}) and
-  then compare them syntactically:
+  Yes: to typecheck, we reduce terms fully (to their \emph{normal form})
+  before comparing:
   \[
   \begin{array}{@{}r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }l}
-    \myunit & \myredd & \myunit & \mydefeq & \myunit & \myreddd & \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \\
-    \myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 & \myredd & \myempty & \mydefeq & \myempty & \myreddd & \myempty \\
+    \myunit & \myredd & \myunit & \mydefeq & \myunit & \myreddd & \myfun{non-empty}\myappsp(3 \mycons \mynil) \\
     (\myabs{\myb{x}\, \myb{y}}{\myb{y}}) \myappsp \myunit \myappsp \myappsp \mynat & \myredd & \mynat & \mydefeq & \mynat & \myreddd & (\myabs{\myb{x}\, \myb{y}}{\myb{x}}) \myappsp \mynat \myappsp \myunit \\
     & & & \vdots & & & 
   \end{array}
   \]
-
-  This equality, $\mydefeq$, takes the name of \emph{definitional} equality.
-  % TODO add break
+  \[
+  \mydefeq\ \text{takes the name of \textbf{definitional equality}.}
+  \]
 \end{frame}
 
 \begin{frame}
   \frametitle{Propositional equality} Using definitional equality, we
   can give the user a type-level notion of term equality.
   \[
-  (\myeq) : \myb{A} \myarr \myb{A} \myarr \mytyp
+  (\myeq) : \myb{A} \myarr \myb{A} \myarr \mytyp\ \ \ \text{internalises equality \textbf{as a type}}
   \]
-  We introduce members of $\myeq$ by reflexivity:
+  We introduce members of $\myeq$ by reflexivity, for example
   \[
-  \myrefl\myappsp\mytmt : \mytmt \myeq \mytmt
+  \myrefl\myappsp5 : 5 \myeq 5
   \]
-  So that $\myrefl$ will relate definitionally equal terms:
+  But also
   \[
-  \myrefl\myappsp 5 : (3 + 2) \myeq (1 + 4)\ \text{since}\ (3 + 2) \myeq (1 + 4) \myredd 5 \myeq 5
+  \begin{array}{@{}l}
+  \myrefl\myappsp 5 : (3 + 2) \myeq (1 + 4)\text{, since}\\
+  (3 + 2) \myeq (1 + 4) \myredd 5 \myeq 5
+  \end{array}
   \]
   Then we can use a substitution law to derive other
   laws---transitivity, congruence, etc.
+  \[ \myeq\ \text{takes the name of \textbf{propositional equality}} \]
 \end{frame}
 
 \begin{frame}
 \frametitle{The problem with prop. equality}
 Going back to $\myfun{map}$, we can prove that
 \[    \forall \myb{f} {:} (\myb{b} \myarr \myb{c}), \myb{g} {:} (\myb{a} \myarr \myb{b}), \myb{l} {:} \mylist{\myb{a}}.\ (\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g}) \myappsp \myb{l} \myeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) \myappsp \myb{l}    \]
-Because we can prove, by induction on $\myb{l}$, that we will always get definitionally equal lists.
+Because
+\[
+(\myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g})\myappsp \myb{l} \mydefeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g}) \myappsp \myb{l}
+\]
+By induction on $\myb{l}$.
 
-But without the $\myb{l}$, we cannot compute, so we are stuck with
+Without the $\myb{l}$ we cannot compute, so we are stuck with
 \[
 \myfun{map}\myappsp \myb{f} \mycomp \myfun{map}\myappsp \myb{g} \not\mydefeq \myfun{map}\myappsp (\myb{f} \mycomp \myb{g})
 \]
@@ -437,17 +438,19 @@ But without the $\myb{l}$, we cannot compute, so we are stuck with
   \frametitle{Observational equality}
 
   Instead of basing its equality on definitional equality, look at the
-  structure of the type to decide:
+  structure of the type to decide.
+
+  For functions this will mean that proving
   \[
-  \begin{array}{@{}l}
-    (\myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g} : \mylistt{\myse{A_1}} \myarr \mylistt{\myse{C_1}}) \myeq (\myfun{map}\myappsp (\myse{f} \mycomp \myse{g}) : \mylistt{\myse{A_2}} \myarr \mylistt{\myse{C_2}}) \myred \\
-    \myind{2} (\myse{l_1} : \mylistt{\myse{A_1}}) \myarr (\myse{l_2} : \mylistt{\myse{A_2}}) \myarr (\myse{l_1} : \mylistt{\myse{A_1}}) \myeq (\myse{l_2} : \mylistt{\myse{A_2}}) \myarr \\
-    \myind{2} ((\myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g}) \myappsp \myse{l} : \mylistt{\myse{C_1}}) \myeq (\myfun{map}\myappsp (\myse{f} \mycomp \myse{g}) \myappsp \myse{l} : \mylistt{\myse{C_2}})
-  \end{array}
+    \myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g} \myeq \myfun{map}\myappsp (\myse{f} \mycomp \myse{g})
+  \]
+  Will reduce to proving that
+  \[
+  (\myb{l} : \mylist{\myb{A}}) \myarr 
+    (\myfun{map}\myappsp \myse{f} \mycomp \myfun{map}\myappsp \myse{g})\myappsp\myb{l} \myeq \myfun{map}\myappsp (\myse{f} \mycomp \myse{g})\myappsp \myb{l}
   \]
-  This extends to other structures (tuples, inductive types, \dots).
-  Moreover, if we can deem two \emph{types} equal, we can \emph{coerce}
-  values from one to the other.
+  Which is what we want.  The interesting part is how to make the system
+  compute nicely.
 \end{frame}
 
 \begin{frame}
@@ -478,29 +481,7 @@ But without the $\myb{l}$, we cannot compute, so we are stuck with
   \[
   \begin{array}{@{}l@{\ }l}
     \mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{pc} \myappsp \mynil & \myred \myse{pn} \\
-    \mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{pc} \myappsp (\mytmm \mycons \mytmn) & \myred \myse{pc} \myappsp \mytmm \myappsp \mytmn \myappsp (\mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{ps} \myappsp \mytmt )
-  \end{array}
-  \]
-\end{frame}
-
-\begin{frame}
-  \frametitle{Records}
-  But also records:
-  \[
-  \mysyn{record}\ \mytyc{Tuple}\myappsp(\myb{A} : \mytyp)\myappsp(\myb{B} : \mytyp) \mapsto \mydc{tuple}\ \{ \myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} \}
-  \]
-  Where each field defines a projection from instances of the record:
-  \[
-  \begin{array}{@{}l@{\ }c@{\ }l}
-    \myfun{fst} & : & \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{A} \\
-    \myfun{snd} & : & \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{B}
-  \end{array}
-  \]
-  Where the projection's reduction rules are predictably
-  \[
-  \begin{array}{@{}l@{\ }l}
-    \myfun{fst}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmm \\
-    \myfun{snd}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmn \\
+    \mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{pc} \myappsp (\mytmm \mycons \mytmn) & \myred \myse{pc} \myappsp \mytmm \myappsp \mytmn \myappsp (\mytyc{List}.\myfun{elim} \myappsp \myse{P} \myappsp \myse{pn} \myappsp \myse{ps} \myappsp \mytmn )
   \end{array}
   \]
 \end{frame}
@@ -523,6 +504,13 @@ But without the $\myb{l}$, we cannot compute, so we are stuck with
     \myfun{snd} & : (\myb{x} : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B}) \myarr \myb{B} \myappsp (\myfun{fst} \myappsp \myb{x})
   \end{array}
   \]
+  Where the projection's reduction rules are predictably
+  \[
+  \begin{array}{@{}l@{\ }l}
+    \myfun{fst}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmm \\
+    \myfun{snd}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmn \\
+  \end{array}
+  \]
 \end{frame}
 
 \begin{frame}
@@ -531,6 +519,8 @@ But without the $\myb{l}$, we cannot compute, so we are stuck with
   % TODO fix
   \[
   \begin{array}{@{}l}
+    \mysyn{data}\ \mynat \mapsto \mydc{zero} \mydcsep \mydc{suc}\myappsp\mynat \\
+    \ \\
     \myfun{even} : \mynat \myarr \mytyp \\
     \begin{array}{@{}l@{\myappsp}c@{\ }l}
       \myfun{even} & \myzero & \mapsto \myunit \\
@@ -551,7 +541,7 @@ But without the $\myb{l}$, we cannot compute, so we are stuck with
   \[
   \cancel{\mytyp : \mytyp}\ \ \ \text{\textbf{inconsistent}}
   \]
-  Much like na{\"i}ve set theory is (Girard's paradox).
+  Similar to Russel's paradox in na{\"i}ve set theory.
 
   Instead, we have a hierarchy:
   \[
@@ -572,6 +562,57 @@ But without the $\myb{l}$, we cannot compute, so we are stuck with
   But in \mykant, you can forget about levels: the consistency is
   checked automatically---a mechanised version of what Russell called
   \emph{typical ambiguity}.
+
+  \begin{center}
+    \begin{tikzpicture}[remember picture, node distance=1.5cm]
+      \begin{pgfonlayer}{foreground}
+      % Place nodes
+      \node (x) {$x$};
+      \node [right of=x] (y) {$y$};
+      \node [right of=y] (z) {$z$};
+      \node [below of=z] (k) {$k$};
+      \node [left  of=k] (j) {$j$};
+      %% Lines
+      \path[->]
+      (x) edge node [above] {$<$}   (y)
+      (y) edge node [above] {$\le$} (z)
+      (z) edge node [right] {$<$}   (k)
+      (k) edge node [below] {$\le$} (j)
+      (j) edge node [left ] {$\le$} (y);
+    \end{pgfonlayer}{foreground}
+    \end{tikzpicture}
+    \begin{tikzpicture}[remember picture, overlay]
+      \begin{pgfonlayer}{background}
+      \fill [red, opacity=0.3, rounded corners]
+      (-2.7,2.6) rectangle (-0.2,0.05)
+      (-4.1,2.4) rectangle (-3.3,1.6);
+    \end{pgfonlayer}{background}
+    \end{tikzpicture}
+  \end{center}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Bidirectional type checking}
+  \[
+  \mysyn{data}\ \mytyc{List}\myappsp (\myb{A} : \mytyp) \mapsto \mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A}\myappsp (\mytyc{List}\myappsp\myb{A})
+  \]
+
+  With no type inference, we have explicit types for the constructors:
+  \[
+  \begin{array}{@{}l@{\ }l}
+    \mydc{nil} & : (\myb{A} : \mytyp) \myarr \mytyc{List}\myappsp\myb{A} \\
+    \mydc{cons} &: (\myb{A} : \mytyp) \myarr \myb{A} \myarr \mytyc{List}\myappsp\myb{A} \myarr \mytyc{List}\myappsp\myb{A}\\
+  \end{array}
+  \]
+  ...ugh:
+  \[
+  \mydc{cons}\myappsp \mynat\myappsp 1 \myappsp (\mydc{cons}\myappsp \mynat \myappsp 2 \myappsp (\mydc{cons}\myappsp \mynat \myappsp 3 \myappsp (\mydc{nil}\myappsp \mynat)))
+  \]
+  Instead, annotate terms and propagate the type:
+  \[
+  \mydc{cons}\myappsp 1 \myappsp (\mydc{cons}\myappsp 2 \myappsp (\mydc{cons} \myappsp 3 \myappsp \mydc{nil})) : \mytyc{List}\myappsp\mynat
+  \]
+  Conversely, when we use eliminators the type can be inferred.
 \end{frame}
 
 \begin{frame}
@@ -581,7 +622,14 @@ But without the $\myb{l}$, we cannot compute, so we are stuck with
   \begin{itemize}
   \item Describe when two types formed by the defined type constructors
     are equal;
+    \[ \mylist{\mytya_1} \myeq \mylist{\mytya_2} \]
   \item Describe when two values of the defined type are equal;
+    \[
+    \begin{array}{@{}c@{\ \ \ \ \ \ }c}
+      \mynil \myeq \mynil & \mynil \myeq \mytmm \mycons \mytmn \\
+      \mytmm \mycons \mytmn \myeq \mynil & \mytmm_1 \mycons \mytmn_1 \myeq \mytmm_2 \mycons \mytmn_2
+    \end{array}
+    \]
   \item Describe how to transport values of the defined type.
   \end{itemize}
 \end{frame}
@@ -595,9 +643,9 @@ But without the $\myb{l}$, we cannot compute, so we are stuck with
   For example we have that
   \[
   \begin{array}{@{}l}
-    ((\myb{x_1} {:} \mytya_1) \myarr \mytyb_1 : \mytyp) \myeq ((\myb{x_2} {:} \mytya_2) \myarr \mytyb_2 : \mytyp) \myred \\
-    \myind{2} (\mytya_1 : \mytyp) \myeq (\mytya_2 : \mytyp) \myand \\
-    \myind{2} (\myb{x_1} : \mytya_1) \myarr (\myb{x_2} : \mytya_2) \myarr (\mytyb_1 : \mytyp) \myeq (\mytyb_2 : \mytyp)
+    \myjm{(\myb{x_1} {:} \mytya_1) \myarr \mytyb_1}{\mytyp}{(\myb{x_2} {:} \mytya_2) \myarr \mytyb_2}{\mytyp} \myred \\ 
+    \myind{2} \myjm{\mytya_1}{\mytyp}{\mytya_2}{\mytyp} \myand  \\
+    \myind{2} ((\myb{x_1} : \mytya_1) \myarr (\myb{x_2} : \mytya_2) \myarr \myjm{\myb{x_1}}{\mytya_1}{\myb{x_2}}{\mytya_2} \myarr \mytyb_1[\myb{x_1}] \myeq \mytyb_2[\myb{x_2}])
   \end{array}
   \]
 
@@ -606,43 +654,40 @@ But without the $\myb{l}$, we cannot compute, so we are stuck with
 \end{frame}
 
 \begin{frame}
-  \frametitle{Bidirectional type checking}
-  \[
-  \mysyn{data}\ \mytyc{List}\myappsp (\myb{A} : \mytyp) \mapsto \mydc{nil} \mydcsep \mydc{cons} \myappsp \myb{A}\myappsp (\mytyc{List}\myappsp\myb{A})
-  \]
+  \frametitle{Bonus!  WebSocket prompt}
+  \url{http://bertus.mazzo.li}, go DDOS it!
 
-  With no type inference, we have explicit types for the constructors:
-  \[
-  \begin{array}{@{}l@{\ }l}
-    \mydc{nil} & : (\myb{A} : \mytyp) \myarr \mytyc{List}\myappsp\myb{A} \\
-    \mydc{cons} &: (\myb{A} : \mytyp) \myarr \myb{A} \myarr \mytyc{List}\myappsp\myb{A} \myarr \mytyc{List}\myappsp\myb{A}\\
-  \end{array}
-  \]
-  ...ugh:
-  \[
-  \mydc{cons}\myappsp \mynat\myappsp 1 \myappsp (\mydc{cons}\myappsp \mynat \myappsp 2 \myappsp (\mydc{cons}\myappsp \mynat \myappsp 3 \myappsp (\mydc{nil}\myappsp \mynat)))
-  \]
-  Instead, annotate terms and propagate the type:
-  \[
-  \mydc{cons}\myappsp 1 \myappsp (\mydc{cons}\myappsp 2 \myappsp (\mydc{cons} \myappsp 3 \myappsp \mydc{nil})) : \mytyc{List}\myappsp\mynat
-  \]
-  Conversely, when we use eliminators the type can be inferred.
+  \includegraphics[width=\textwidth]{web-prompt.png}
 \end{frame}
 
 \begin{frame}
-  \frametitle{Bidirectional type checking}
+\begin{center}
+{\Huge Demo}
+\end{center}
+\end{frame}
 
-  This technique is known as \emph{bidirectional} type checking---some
-  terms get \emph{checked}, some terms \emph{infer} types.
+\begin{frame}
+  \frametitle{What have we done?}
 
-  Usually used for pre-defined types or core calculi, \mykant\ extends
-  to user-defined types.
+  \begin{itemize}
+    \item A small theorem prover for intuitionistic logic, featuring:
+    \item Inductive data and record types;
+    \item A cumulative, implicit type hierarchy;
+    \item Partial type inference---bidirectional type checking;
+    \item Type holes;
+    \item Observational equality---coming soon to the implementation.
+  \end{itemize}
 \end{frame}
 
 \begin{frame}
-\begin{center}
-{\Huge Demo}
-\end{center}
+  \frametitle{Further work}
+
+  \begin{itemize}
+    \item Pattern matching and explicit recursion
+    \item More expressive data types
+    \item Inference via unification
+    \item Codata
+  \end{itemize}
 \end{frame}
 
 \begin{frame}