Value type spec.

slides.tex

@@ -29,12 +29,14 @@
 \newcommand{\stores}{\operatorname{Store}}
 \newcommand{\states}{\operatorname{State}}
 \newcommand{\traces}{\operatorname{Trace}}
+\newcommand{\types}{\operatorname{Type}}
 \newcommand{\state}[2]{\langle{} #1, #2 \rangle{}}
 \newcommand{\guard}[1]{\operatorname{guard} E_{#1}}
 \newcommand{\gu}[1]{\operatorname{G} E_{#1}}
 \newcommand{\extr}[1]{\operatorname{extr}_{#1}}
 
 \newcommand{\hot}[1]{\operatorname{hot}_{#1}}
+\newcommand{\evexpT}[2]{\mathbf{E}^t\left(#1\right)_{#2}}
 
 \newcommand*\oldmacro{}%
 \let\oldmacro\insertshorttitle%
@@ -252,6 +254,10 @@
 
         \item Formally define an operator \alert{$\extr{hp}(P)$} extracting the
             hot path $hp$ from the program $P$
+            \vspace{1em}
+
+        \item Once the hot path is extracted, it can be \alert{optimized}
+            \wrt{} known store restrictions.
     \end{itemize}
 \end{frame}
 
@@ -321,7 +327,25 @@
 \end{frame}
 
 \begin{frame}{Value type specialization}
-    %TODO
+    \begin{itemize}
+        \item Seen again as \alert{abstract interpretation}: define $\alpha,
+            \gamma$.
+        \item First, consider \alert{abstract type stores} $\stores^t := \vars
+            \to \types$
+            \begin{itemize}
+                \item Clearly a valid abstract domain for $\stores$
+            \end{itemize}
+
+        \item Then, an operator \alert{$\evexpT{E}{\rho}$} $: \exprs \to
+            \stores^t \to \types$ typing an expression (possibly to Undef or
+            $\Omega$)
+
+        \item Finally, define type specialization \alert{$TS_{hp}$} as the
+            substitution in $hp$ of $+$ by its typed alternative, if possible
+            \\
+            {\small (\ie{} $\evexpT{E + E'}{\rho} \in \set{\text{Int},
+            \text{String}}$)}
+    \end{itemize}
 \end{frame}
 
 \section{Correctness proof}