From 2ae3e1aa2b219696f57b8e2bcbb09146174fa43d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= <contact@tobast.fr>
Date: Mon, 5 Mar 2018 00:29:59 +0100
Subject: [PATCH] Add correctness proof sketches

---
 slides.tex | 37 +++++++++++++++++++++++++++++++++++--
 1 file changed, 35 insertions(+), 2 deletions(-)

diff --git a/slides.tex b/slides.tex
index 45755b2..d0d3f9e 100644
--- a/slides.tex
+++ b/slides.tex
@@ -376,9 +376,43 @@
 \end{frame}
 
 \begin{frame}{Correctness proof sketch, trace extraction}
+    \begin{block}{Theorem}
+        Trace extraction is correct \wrt{} $\alpha_{sc}$, that is, $\forall P,
+        \forall hp$,
+        \[ \alpha_{sc}(\tracesOf(P)) = \alpha_{sc}(\tracesOf(\extr{hp}(P))) \]
+    \end{block}
+    \begin{itemize}
+        \item Proved by mapping $\sigma \in \traces$ to its correct trace
+            through $tr_{hp}(\sigma)$ in $\extr{hp}(P) =: P_{hp}$
+
+        \item Then show that
+            \begin{enumerate}[i]
+                \item $tr_{hp}(\tracesOf(P)) \subseteq \tracesOf(P_{hp})$
+                \item $\alpha_{sc}(\tracesOf(P_{hp}))
+                    \subseteq \alpha_{sc}(\tracesOf(P))$
+                \item $\alpha_{sc} \circ tr_{hp} = \alpha_{sc}$
+            \end{enumerate}
+    \end{itemize}
 \end{frame}
 
 \begin{frame}{Correctness proof sketch, type specialization}
+    \begin{block}{Theorem}
+        Type specialization is correct (at traces level)
+    \end{block}
+
+    \begin{itemize}
+        \item Define $tt(\sigma)$ erasing type specialization (\eg{}
+            $+_{\text{Int}} \mapsto +$).
+        \item Then, $tt(\tracesOf(TS_{hp}(stitch_P(hp)))) =
+            \tracesOf(stitch_P(hp))$
+    \end{itemize}
+
+    \begin{block}{Theorem}
+        Stitching type specialization to a hot path is correct \wrt{}
+        $\alpha_{sc}$.
+    \end{block}
+
+    (directly follows)
 \end{frame}
 
 \section*{}
@@ -400,8 +434,7 @@
                     \alert{pretends otherwise}
                 \item Unusably \alert{small toy language}
                 \item Absurdly \alert{hard to read} toy language
-                \item Proof \wrt{} some $\alpha$ which is not
-                    \textit{that} realistic
+                \item Proof \wrt{} some $\alpha$ which does not handle effects
                 \item Please, stop claiming every line or two that your paper
                     is better than Guo and Palsberg's
             \end{itemize}