Define toy language

slides.tex

@@ -16,6 +16,16 @@
 
 \newcommand{\wrt}{\textit{wrt.}}
 
+\newcommand{\progs}{\mathbb{P}}
+\newcommand{\labels}{\mathbb{L}}
+\newcommand{\values}{\mathbb{K}}
+\newcommand{\vars}{\mathcal{V}}
+\newcommand{\exprs}{\text{Expr}}
+\newcommand{\bexprs}{\text{BExpr}}
+\newcommand{\actions}{\mathbb{A}}
+\newcommand{\commands}{\mathbb{C}}
+\newcommand{\askip}{\operatorname{skip}}
+
 \newcommand*\oldmacro{}%
 \let\oldmacro\insertshorttitle%
 \renewcommand*\insertshorttitle{%
@@ -104,43 +114,94 @@
 \section{Study setup}
 
 \begin{frame}{Study objectives}
+    \begin{itemize}
+        \item Formalism to see JIT as AbsInt (\textit{online source
+            transformation})
+            \begin{itemize}
+                \item Hot path extraction
+                \item Type specialization
+            \end{itemize}
+            \vspace{1em}
+
+        \item Formalism to extract observables from code\\
+            $\leadsto$ compare observables with/without JIT\\
+            $\leadsto$ prove correctness
+            \vspace{1em}
+
+        \item Can be extended with virtually any feature
+    \end{itemize}
 \end{frame}
 
 \begin{frame}{Studied language}
+    \begin{columns}[c]
+        \column{0.5\textwidth}
+        \begin{itemize}
+            \item $\labels$: program labels
+            \item $\values$: literal values
+            \item $\vars$: variables
+            \item $(\progs := \commands \text{ list})$: programs
+        \end{itemize}
+        \begin{align*}
+            C &::= L : A \to L' &\commands \\
+            A &::=
+                (x := E)\,\vert\,B\,\vert\,\askip &\actions \\
+            E, E' &::= v\,\vert\,x\,\vert\,E + E' &\exprs \\
+            B, B' &::= \top\,\vert\,\bot\,\vert\,E \leq E' & \bexprs \\
+                &\qquad\vert\,\lnot B\,\vert\,B \wedge B'
+        \end{align*}
+
+        \column{0.5\textwidth}
+        \begin{itemize}
+            \item Conditional:
+                \begin{align*}
+                    l_0&: b_0 \to l_{t} \\
+                    l_0&: \lnot b_0 \to l_{f}
+                \end{align*}
+            \item Turing-complete
+            \item Supposed to model some bytecode
+        \end{itemize}
+    \end{columns}
 \end{frame}
 
 \section{Abstract interpretation}
 
 \begin{frame}{AbsInt hot path extraction}
+    %TODO
 \end{frame}
 
 \begin{frame}{Value type specialization}
+    %TODO
 \end{frame}
 
 \section{Correctness proof}
 
 \begin{frame}{Correctness proof sketch}
+    %TODO
 \end{frame}
 
 \section*{Conclusion}
 
-\begin{frame}{Conclusion}
+\begin{frame}[shrink]{Conclusion}
     \begin{columns}[c]
         \column{.8 \textwidth}
         \begin{exampleblock}{Pros}
             \begin{itemize}
-                \item Opens the way for AbsInt formalism in JIT
-                \item Provides an (implemented?) framework for JIT study
+                \item Opens the way for \alert{AbsInt formalism} in JIT
+                \item Provides an (implemented?) \alert{framework} for JIT
+                    study
             \end{itemize}
         \end{exampleblock}
 
         \begin{alertblock}{Cons}
             \begin{itemize}
-                \item Overly restrictive in JIT features, pretends otherwise
-                \item Unusably small toy language
-                \item Absurdly hard to read toy language
+                \item \alert{Overly restrictive} in JIT features,
+                    \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 much} realistic
+                    \textit{that} realistic
+                \item Please, stop claiming every line or two that your paper is
+                    better than Guo and Palsberg's
             \end{itemize}
         \end{alertblock}