Add correctness proof sketch (1)

slides.tex

@@ -37,6 +37,7 @@
 
 \newcommand{\hot}[1]{\operatorname{hot}_{#1}}
 \newcommand{\evexpT}[2]{\mathbf{E}^t\left(#1\right)_{#2}}
+\newcommand{\tracesOf}{\mathbf{T}}
 
 \newcommand*\oldmacro{}%
 \let\oldmacro\insertshorttitle%
@@ -351,7 +352,33 @@
 \section{Correctness proof}
 
 \begin{frame}{Correctness proof sketch}
-    %TODO
+    \begin{itemize}
+        \item Idea: define (cf. Cousot) correctness of transformation as
+            \alert{observational equivalence} of source and transformed
+            programs \alert{\wrt{} some abstraction} $\alpha:
+            \powerset(\traces) \to \powerset(\stores^\ast)$.
+        \item That is, if $\alpha$ derives the abstraction, $\tracesOf$
+            extracts the program traces and $Tr$ transforms it, we want
+            \[ \alpha(\tracesOf(P)) = \alpha(\tracesOf(Tr(P))) \]
+        \item Heavy but safe: $\alpha = \alpha_{sc}$, \alert{store changes}
+            \[
+                sc(s_1 s_2 \sigma) := \left\{
+                    \begin{array}{l l}
+                        St(s_1) \cdot sc(s_2 \sigma), &
+                            St(s_1) \neq St(s_2) \\
+                        sc(s_2 \sigma), &
+                            St(s_1) = St(s_2)
+                    \end{array}
+                    \right.
+            \]
+        \item Lighter: same, but only at \alert{loop entry/exit points}
+    \end{itemize}
+\end{frame}
+
+\begin{frame}{Correctness proof sketch, trace extraction}
+\end{frame}
+
+\begin{frame}{Correctness proof sketch, type specialization}
 \end{frame}
 
 \section*{}
@@ -375,8 +402,8 @@
                 \item Absurdly \alert{hard to read} toy language
                 \item Proof \wrt{} some $\alpha$ which is not
                     \textit{that} realistic
-                \item Please, stop claiming every line or two that your paper is
-                    better than Guo and Palsberg's
+                \item Please, stop claiming every line or two that your paper
+                    is better than Guo and Palsberg's
             \end{itemize}
         \end{alertblock}