diff --git a/slides/Makefile b/slides/Makefile
index 98b3eaa..db66653 100644
--- a/slides/Makefile
+++ b/slides/Makefile
@@ -1,6 +1,10 @@
 TEX=slides.tex
+BASE=slides
 all: $(TEX)
 	pdflatex $(TEX)
 	pdflatex $(TEX)
 
+upload:
+	scp $(BASE).pdf www.tobast:~/tobast.fr/public_html/l3/slides.pdf
+
 
diff --git a/slides/slides.tex b/slides/slides.tex
index c56860c..28f5374 100644
--- a/slides/slides.tex
+++ b/slides/slides.tex
@@ -228,7 +228,7 @@ jeux}
 	\begin{definition}{structure d'événement (déterministe)}
 		$(E, \leq_E)$ ensemble d'\emph{événements} partiellement ordonné.
 	\end{definition}
-	-\pause%
+	\pause%
 	\begin{definition}{structure d'événement polarisée (SEP) / \alert{jeu}}
 		$(E, \leq_E, \rho_E)$ où $(E, \leq_E)$ est une structure d'événements
 		et $\rho_E : E \to \set{\ominus, \oplus}$.
@@ -286,12 +286,24 @@ jeux}
 
 \section{Interprétation de \llccs}
 
+\subsection{Sémantique dénotationnelle}
+
 \begin{frame}{Interprétation de \llccs}
-	\begin{columns}[t]
+	\begin{columns}[c]
 		\column{0.5\textwidth}
 
 		\begin{align*}
-			\seman{\proc} &\eqdef 
+			\seman{\proc} &\eqdef \begin{tikzpicture}[baseline]
+				\node (1) at (0,0.5) [draw=red,ellipse] {call};
+				\node (2) at (0,-0.5) [draw=green,ellipse] {done};
+				\draw [->] (1) -- (2);
+			\end{tikzpicture}
+			= \seman{\chan} \\
+			%
+			\seman{1} &\eqdef \seman{P} \\
+			\seman{0} &\eqdef \begin{tikzpicture}[baseline]
+				\node (1) at (0,0.2) [draw=red,ellipse] {call};
+			\end{tikzpicture}
 		\end{align*}
 
 		\column{0.5\textwidth}
@@ -304,6 +316,81 @@ jeux}
 			\seman{\lambda x^A \cdot t} &\eqdef \seman{t}
 		\end{align*}
 	\end{columns}
+
+	\vspace{1em}
+	\hrule{}
+	\vspace{0.5em}
+
+	\emph{Suit les règles de typage}~:
+	\[
+		u_1 : A_1, \ldots, u_p : A_p \vdash t : B \implies \seman{t} :
+		\seman{A_1}^\perp \parallel \ldots \parallel \seman{A_p}^\perp
+		\parallel \seman{B}
+	\]
+\end{frame}
+
+\subsection{Adequacy}
+
+\begin{frame}{Adequacy}
+	\begin{theorem}{adequacy}
+		La sémantique dénotationnelle est \emph{adéquate} à la sémantique
+		opérationnelle, \ie{}
+		\[
+			\forall P\,/\,(\vdash P : \proc),~(P \redarrow{\tau}^\ast 1) \iff
+			(\seman{P} = \seman{1})
+		\]
+	\end{theorem}
+\end{frame}
+
+\begin{frame}{Adequacy, preuve}
+	\begin{itemize}
+		\item Sens direct~: induction sur $P \redarrow{\tau}^\ast 1$, en
+			utilisant une induction auxiliaire~: $\forall P \redarrow{x} Q,\,
+			\forall l \in \mathcal{L}_{P \redarrow{x} Q}$,
+			\begin{itemize}
+				\item si $x = \tau$, $\seman{P}_l = \seman{Q}_l$~;
+				\item si $x = a : \chan$, $\seman{P} = \seman{a \cdot Q}_l$~;
+				\item si $x = \tau_a$, $\seman{P}_{a::l} = \seman{Q}_l$~;
+			\end{itemize}
+			où $\seman{u}_{h::t} \eqdef \seman{\newch{h}u}_t$, $\seman{u}_{[]}
+			\eqdef \seman{u}$.
+		\pause\vspace{1em}
+		\item Sens réciproque~: on prouve par induction sur la syntaxe la
+			contraposée, $P \neq 1 \land \seman{P} = \seman{1} \implies P
+			\redarrow{\tau}$.
+	\end{itemize}
+\end{frame}
+
+\section{Implémentation}
+
+\begin{frame}{Implémentation --- backend}
+	\begin{itemize}
+		\item Implémentation des opérations sur jeux/stratégies
+		\item Utilisable comme backend ou en toplevel
+		\item Représentation Dot de jeux/stratégies
+		\item Essentiellement OCaml
+		\item SLOCCount~: 2330 lignes
+		\item Nécessité de travailler très formellement (associativité, \ldots)
+	\end{itemize}
+\end{frame}
+
+\begin{frame}{Frontend \llccs}
+	\begin{itemize}
+		\item Parseur/lexeur \llccs{}
+		\item Transformation des termes en stratégies
+		\item Passage par le backend $\leadsto$ stratégie
+		\item Adequacy~: permet de décider si $P \redarrow{\tau}^\ast 1$
+		\item Frontend javascript~: entrée de stratégie et retour graphique sur
+			page web
+	\end{itemize}
+	\vfill
+	\hfill\url{https://tobast.fr/l3/demo.html}
+\end{frame}
+
+\section*{}
+
+\begin{frame}{Conclusion}
+	\begin{center}\begin{Huge}Merci~!\end{Huge}\end{center}
 \end{frame}
 
 \end{document}
diff --git a/slides/theorems.sty b/slides/theorems.sty
index 535b2a1..70ce9b6 100644
--- a/slides/theorems.sty
+++ b/slides/theorems.sty
@@ -1,5 +1,5 @@
 % vim: :spell spelllang=fr
 
 \renewenvironment{definition}[1]{\begin{block}{Définition~: #1.}}{\end{block}}
-\renewenvironment{theorem}[1]{\begin{block}{Théorème~: #1.}}{\end{block}}
+\renewenvironment{theorem}[1]{\begin{alertblock}{Théorème~: #1.}}{\end{alertblock}}
 \renewenvironment{lemma}[1]{\begin{block}{Lemme~: #1.}}{\end{block}}