From 7ad40c8cf3d36ee1bc3f45233c15e1dfb24dc729 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= <contact@tobast.fr>
Date: Sun, 4 Mar 2018 17:39:18 +0100
Subject: [PATCH] Describe types, values, rough semantics

---
 slides.tex | 57 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 57 insertions(+)

diff --git a/slides.tex b/slides.tex
index 05ef6a8..70b7ee3 100644
--- a/slides.tex
+++ b/slides.tex
@@ -25,6 +25,10 @@
 \newcommand{\actions}{\mathbb{A}}
 \newcommand{\commands}{\mathbb{C}}
 \newcommand{\askip}{\operatorname{skip}}
+\newcommand{\stores}{\operatorname{Store}}
+\newcommand{\states}{\operatorname{State}}
+\newcommand{\traces}{\operatorname{Trace}}
+\newcommand{\state}[2]{\langle{} #1, #2 \rangle{}}
 
 \newcommand*\oldmacro{}%
 \let\oldmacro\insertshorttitle%
@@ -163,6 +167,59 @@
     \end{columns}
 \end{frame}
 
+\begin{frame}{Types, rough semantics}
+    \hspace*{-1em}\textbf{Types \& values}
+
+    \begin{columns}[c]
+        \column{0.6\textwidth}
+        \begin{itemize}
+            \item $\values\,:=\,\relset \cup \set{a, \ldots, z}^\ast$
+            \item Types: Int, String, Undef, $\emptyset$, $\Omega$
+            \item Undef: error type
+        \end{itemize}
+
+        \column{0.4\textwidth}
+        \begin{center}
+            \begin{tikzpicture}{c}
+                \node (E) at (0, 0) {$\emptyset$};
+                \node (I) at (-1.5, 1) {Int};
+                \node (S) at (0, 1) {String};
+                \node (U) at (1.5, 1) {Undef};
+                \node (T) at (0, 2) {$\Omega$};
+                \draw[->] (E) -- (I);
+                \draw[->] (E) -- (S);
+                \draw[->] (E) -- (U);
+                \draw[<-] (T) -- (I);
+                \draw[<-] (T) -- (S);
+                \draw[<-] (T) -- (U);
+            \end{tikzpicture}
+        \end{center}
+    \end{columns}
+
+    \vspace{1em}
+    \hspace*{-1em}\textbf{Semantics}
+
+    \begin{columns}[c]
+        \column{.5\textwidth}
+
+        \begin{itemize}
+            \item Type-dependant $+$:
+                \begin{itemize}
+                    \item $+_{String}$: concatenation
+                    \item $+_{Int}$: usual $+$
+                    \item $+_{Str, Int}$: yields Undef
+                \end{itemize}
+        \end{itemize}
+
+        \column{.5\textwidth}
+        \begin{align*}
+            \stores &:= \vars \to \values & \rho \\
+            \states &:= \commands \times \stores & \state{C}{\rho} \\
+            \traces &:= \states^\ast
+        \end{align*}
+    \end{columns}
+\end{frame}
+
 \section{Abstract interpretation}
 
 \begin{frame}{AbsInt hot path extraction}