Makefile: upload > all

report/biblio.bib

@@ -34,7 +34,7 @@
 }
 
 @article{abramsky2000pcf,
-  title={Full abstraction for PCF},
+  title={{Full abstraction for PCF}},
   author={Abramsky, Samson and Jagadeesan, Radha and Malacaria, Pasquale},
   journal={Information and Computation},
   volume={163},
@@ -82,7 +82,7 @@
 }
 
 @article{laird2001game,
-  title={A game semantics of Idealized CSP},
+  title={{A game semantics of Idealized CSP}},
   author={Laird, James},
   journal={Electronic Notes in Theoretical Computer Science},
   volume={45},

report/my_hyperref.sty

@@ -1,7 +1,8 @@
 \usepackage{hyperref}
-\usepackage[dvipsnames]{xcolor}
+\usepackage{xcolor}
 
 \definecolor{link_blue}{RGB}{0,0,97}
+\definecolor{cite_green}{HTML}{009B55}
 
 \hypersetup{
 %    bookmarks=true,         % show bookmarks bar?
@@ -19,7 +20,7 @@
 %    pdfnewwindow=true,      % links in new PDF window
     colorlinks=true,       % false: boxed links; true: colored links
     linkcolor=link_blue,          % color of internal links (change box color with linkbordercolor)
-    citecolor=ForestGreen,        % color of links to bibliography
+    citecolor=cite_green,        % color of links to bibliography
     filecolor=magenta,      % color of file links
     urlcolor=link_blue           % color of external links
 }

report/report.tex

@@ -83,14 +83,13 @@ the two strategies.
 
 \paragraph{Concurrency in game semantics.} In the continuity of the efforts put
 forward to model imperative primitives in game semantics, it was natural to
-focus at some point on modelling concurrency. The problem was tackled by
+focus at some point on modelling concurrency. The problem was first tackled by
 \fname{Laird}~\cite{laird2001game}, introducing game semantics for a \lcalc{}
 with a few additions, as well as a \emph{parallel execution} operator and
-communication on channels. It is often considered, though, that \fname{Ghica}
-and \fname{Murawski}~\cite{ghica2004angelic} really took the fundamental step
-by defining game semantics for a fine-grained concurrent language including
-parallel execution of ``threads'' and low-level semaphores --- a way more
-realistic approach to the problem.
+communication on channels. \fname{Ghica} and \fname{Murawski} then simplified
+\textsc{Laird}'s approach, and gave a fully abstract model for a slightly more
+realistic concurrent programming language with shared memory
+in~\cite{ghica2004angelic}.
 
 However, both of these constructions are based on \emph{interleavings}. That
 is, they model programs on \emph{tree-like games}, games in which the moves
@@ -105,15 +104,15 @@ combination of moves is a valid path.
 
 However, this approach introduces non-determinism in the strategies: if two
 moves are available to a player, the model states that they make a
-non-deterministic uniform choice. Yet, one could reasonably argue that a
-program should behave consistently with the environment, which would mean that
-the semantics of a program --- even a concurrent one --- should still be
-deterministic. This idea was explored outside of the game semantics context,
-for instance by~\cite{reynolds1978syntactic}, establishing a type-checking
-system to restrict concurrent programs to deterministic ones. Some recent work
-makes use of linear logic~\cite{caires2010session} for similar purposes as
-well.  Yet, the interleavings game semantics of these languages remains
-non-deterministic.
+non-deterministic uniform choice.  Yet, even for concurrent programs it is
+often a desirable property that they should behave consistently with the
+environment, meaning that they are deterministic up to the choice of the
+scheduler.  Such determinism can be ensured statically, via typing. This idea
+was explored outside of the game semantics context, for instance
+by~\cite{reynolds1978syntactic}, establishing a type-checking system to
+restrict concurrent programs to deterministic ones. Some recent work makes use
+of linear logic~\cite{caires2010session} for similar purposes as well.  Yet,
+the interleavings game semantics of these languages remains non-deterministic.
 
 \paragraph{The purpose of this internship} was to try to take a first step
 towards the reunification of those two developments. For that purpose, my
@@ -142,7 +141,7 @@ synchronization of processes through \emph{channels} ---, lifted up to the
 higher order through a \lcalc. The language was then restricted to a
 \emph{linear} one --- that is, each identifier declared must be referred to
 exactly once ---, partly to keep the model simple, partly to meet the
-determinism requirements.
+determinism requirements through the banning of interference.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \subsection{A linear variant of CCS~: \linccs}
@@ -231,7 +230,7 @@ where $a$ denotes a channel and $x$ denotes any possible label.
 		\frac{P \redarrow{x} P'}
 			{P \cdot Q \redarrow{x} P' \cdot Q} & &
 		\frac{P \redarrow{x} P'}
-			{(\nu a)P \redarrow{x} (\nu a)P'} & (a \not\in \set{x,\tau_a})
+			{(\nu a)P \redarrow{x} (\nu a)P'} & (x \not\in \set{a,\tau_a})
 	\end{align*}
 	\caption{\linccs{} operational semantics}\label{fig:lccs:opsem}
 \end{figure}
@@ -245,11 +244,7 @@ necessary. Consider the reduction of $(\nu a) (a \cdot 1 \parallel \bar{a}
 to reduce to $1$; but if we replaced that $\tau_a$ with a $\tau$, the whole
 term would reduce to $(\nu a) 1$, which has no valid type since $a$ and
 $\bar{a}$ are not consumed (linearity). Our semantics would then not satisfy
-subject reduction.
-
-Switching to an \emph{affine} \linccs{} while keeping it wrapped in a
-\emph{linear} \lcalc{} was considered, but yielded way too many problems, while
-switching to a fully-affine model would have modified the problem too deeply.
+subject reduction for $\tau$-reductions.
 
 \subsection{Lifting to the higher order: linear \lcalc}
 
@@ -257,7 +252,7 @@ In order to reach the studied language, \llccs, we have to lift up \linccs{} to
 a \lcalc. To do so, we add to the language the constructions of
 figure~\ref{fig:llam:syntax}, which are basically the usual \lcalc{}
 constructions slightly transformed to be linear (which is mostly reflected by
-the typing rules). In particular, the only base types are $\proc$ and $\chan$.
+the typing rules).
 
 \begin{figure}[h]
 	\begin{minipage}[t]{0.55\textwidth}
@@ -338,15 +333,17 @@ To lift the operational semantics to \llccs, we only need to add one rule:
 		\left(\left(\left(\bar{f} \cdot 1\right) \cdot
 		\left(\bar{g} \cdot 1\right)\right) \parallel \left(g \cdot 1\right)
 		\right)\right)$. Note that the function has no idea whether two
-		channels are dual or not.
+		channels are dual or not, that is, its declaration ignores duality
+		relations between its parameters. In practice, it means that no
+		synchronization can happen before the term is $\beta$-reduced.
 \end{itemize}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \section{A games model}
 
-Our goal is now to give a games model for the above language. For that purpose,
-we will use \emph{event structures}, providing an alternative formalism to
-the often-used tree-like games.
+Our goal is now to give a deterministic games model for the above language. For
+that purpose, we will use \emph{event structures}, providing an alternative
+formalism to the often-used tree-like games.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \subsection{The event structures framework}
@@ -371,9 +368,9 @@ corresponds to the game tree
 \]
 
 This can of course be used to describe much larger games, and is often useful
-to reason concurrently, since the causal histories appears clearly: the
-possible states of the game can be read easily by concatenating the events
-found along a path from the root of the tree.
+to reason concurrently. The different configurations of the game that can be
+reached are quite easily read: one only has to concatenate the events found
+along path starting at the root of the tree.
 
 But it also has the major drawback of growing exponentially in size: let us
 consider a game in which Opponent must play $A$ and $B$ in no particular order
@@ -395,10 +392,14 @@ before Player can play $C$. The corresponding tree-like game would be
 	\end{tikzpicture}
 \]
 
-This goes even worse with less structure: since there is $n!$ % chktex 40
+This goes even worse with less structure: since there are $n!$ % chktex 40
 permutations for $n$ elements, the tree can grow way larger.
 
-This problem motivated the use of \emph{event structures} as a formalism to
+The previous example also points out a kind of \textit{obfuscation} of the
+causal histories: reading the diagram above does not make it obvious to the
+reader that $A$ and $B$ must be played before $C$.
+
+This problem can be solved by using \emph{event structures} as a formalism to
 describe such games~\cite{rideau2011concurrent}. Informally, an event structure
 is a partial order $\leq$ on \emph{events} (here, the game's moves), alongside
 with a \emph{consistency} relation.
@@ -433,7 +434,9 @@ look like
 	\leq_E e}$ is finite.
 
 	The partial order $\leq_E$ naturally induces a binary relation $\edgeArrow$
-	over $E$ that is defined as the transitive reduction of $\leq_E$.
+	over $E$ that is defined as the transitive reduction of $\leq_E$, \ie{} the
+	minimal subset of $\leq_E$ such that the transitive closures of $\leq_E$
+	and $\edgeArrow$ are the same.
 \end{definition}
 
 In this context, the right intuition of event structures is a set of events
@@ -442,7 +445,7 @@ a given move cannot occur before another move.
 
 Event structures are often represented as a directed acyclic graph (DAG)
 where the vertices are the elements of $E$ and the edges are the transitive
-reduction of $\leq_E$.
+reduction of $\leq_E$ (\ie{} $\edgeArrow_E$).
 
 \begin{definition}[event structure with polarities]
 	An \emph{event structure with polarities} (\textit{ESP}) is an event
@@ -485,8 +488,9 @@ strategies.
 \begin{notation}
 	For $x,y \in \config(A)$, $x \forkover{e} y$ states that $y =
 	x \sqcup \set{e}$ (and that both are valid configurations), where $\sqcup$
-	denotes the disjoint union. It is also possible to write $x \forkover{e}$,
-	stating that $x \sqcup \set{e} \in \config(A)$, or $x \fork y$.
+	is used to mean that the standard union ($\cup$) is disjoint. It is also
+	possible to write $x \forkover{e}$, stating that $x \sqcup \set{e} \in
+	\config(A)$, or $x \fork y$.
 \end{notation}
 
 %%%%%
@@ -534,7 +538,7 @@ drink.
 	\]
 	The ``call'' event will be triggered by Opponent (the system) when the
 	process is started, and Player will play ``done'' when the process has
-	finished, if it ever does. The relation $\text{call} \leq \text{done}$
+	finished, if it ever does. The relation $\texttt{call} \leq \texttt{done}$
 	means that a process cannot finish \emph{before} it is called: unlike what
 	happened in	the previous example, it is here a ``hardwired'' relation that
 	the software cannot bypass.
@@ -544,7 +548,8 @@ drink.
 	A \emph{pre-strategy} on the game $A$, written $\sigma: A$, is an ESP such
 	that
 	\begin{enumerate}[(i)]
-		\item $\sigma \subseteq A$;
+		\item $\sigma \subseteq A$ (inclusion over set of events, not including
+			the order);
 		\item $\config(\sigma) \subseteq \config(A)$;
 		\item $\forall s \in \sigma, \rho_A(s) = \rho_\sigma(s)$
 	\end{enumerate}
@@ -600,23 +605,26 @@ int main() {
 
 But as it is defined, a pre-strategy does not exactly capture what we expect of
 a \emph{strategy}: it is too expressive. For instance, the relation
-$\text{call}_0 \leq \text{call}_1$ on the above strategy is allowed, stating
-that the operating system cannot decide to start the process $1$ before the
-process $0$. It is not up to the program to decide that, this strategy is thus
-unrealistic. We then have to restrict pre-strategies to \emph{strategies}:
+$\text{call}_0 \leq \text{call}_1$ on a variant of the above strategy would be
+allowed, stating that the operating system cannot decide to start the process
+$1$ before the process $0$. It is not up to the program to decide that, this
+strategy is thus unrealistic. We then have to restrict pre-strategies to
+\emph{strategies}:
 
 \begin{definition}[strategy]
 	A \emph{strategy} is a pre-strategy $\sigma : A$ that
 	``behaves well'', \ie{} that is
 	\begin{enumerate}[(i)]
 		\item\label{def:receptive}
-			\textit{receptive}: for all $x \in \config(A)$ \st{}
-			$x \forkover{e^-}$, $e \in \sigma$;
+			\textit{receptive}: $\forall x \in \config(\sigma), x \sqcup
+			\set{e} \in \config(A) \land \rho(e) = \ominus \implies x \sqcup
+			\set{e} \in \config(\sigma)$
+
 
 		\item\label{def:courteous}
-			\textit{courteous}: $\forall x \edgeArrow_\sigma x' \in \sigma$,
-			$(\rho(x),\rho(x')) \neq (-,+) \implies
-			x \edgeArrow_A x'$.
+			\textit{courteous}: $\forall e \edgeArrow_\sigma e' \in \sigma$,
+			$(\rho(e),\rho(e')) \neq (-,+) \implies
+			e \edgeArrow_A e'$.
 	\end{enumerate}
 \end{definition}
 
@@ -634,8 +642,8 @@ to consider an arrow ${\ostar \edgeArrow \ominus}$, which would mean forcing
 Opponent to wait for a move (either from Player or Opponent) before playing
 their move; but ${\oplus \edgeArrow \oplus}$ is also unreasonable, since we're
 working in a concurrent context. Intuitively, one could think that when playing
-$x$ then $y$, it is undefined whether Opponent will receive $x$ then $y$ or $y$
-then $x$.
+$e$ then $e'$, it is undefined whether Opponent will receive $e$ then $e'$ or
+$e'$ then $e$.
 
 %%%%%
 \subsubsection{Operations on games and strategies}\label{sssec:es_operations}
@@ -680,7 +688,7 @@ one strategy plays against the other''.
 	${(\leq_\sigma \cup \leq_\tau)}^\ast$ (transitive closure) that may not
 	respect antisymmetry, that is, may have causal loops. The event structure
 	$\sigma \wedge \tau$ is then obtained by removing all the elements
-	contained in such loops from $\sigma \cap \tau$, yielding a regular order.
+	contained in such loops from $\sigma \cap \tau$, yielding a partial order.
 \end{definition}
 
 \textit{This construction is a simplified version of the analogous one
@@ -707,8 +715,8 @@ f$).
 \begin{definition}[compositional interaction]
 	Given two strategies $\sigma : A^\perp \parallel B$ and $\tau : B^\perp
 	\parallel C$, their \emph{compositional interaction} $\tau \strInteract
-	\sigma$ is an event structure defined as $(\sigma \parallel C) \wedge
-	(A^\perp \parallel \tau)$, where $A^\perp$ and $C$ are seen as strategies.
+	\sigma$ is an event structure defined as $(\sigma \parallel C^\perp) \wedge
+	(A \parallel \tau)$, where $A$ and $C^\perp$ are seen as strategies.
 \end{definition}
 
 The idea is to put in correspondence the ``middle'' states (those of $B$) while
@@ -746,7 +754,8 @@ the other player from each board on the other.
 
 The copycat strategy of a game is indeed an identity for the composition of
 \emph{strategies}. In fact, it even holds that for a \emph{pre-}strategy
-$\sigma : A$, $\sigma$ is a strategy $\iff$ $\cc_A \strComp \sigma = \sigma$.
+$\sigma : A$, $\sigma$ is a strategy $\iff$ $\cc_A \strComp \sigma =
+\sigma$~\cite{rideau2011concurrent}.
 
 \begin{example}[copycat]
 	If we consider the following game $A$
@@ -808,8 +817,7 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}.
 				\node (0) at (5,0.65) [draw=red,ellipse] {call};
 				\node (1) at (5,-0.65) [draw=green,ellipse] {done};
 				\path[->]
-					(0) edge (1)
-						edge [bend right] (2)
+					(0)	edge [bend right] (2)
 						edge [bend right] (4)
 					(2) edge (3)
 					(4) edge (5)
@@ -832,8 +840,7 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}.
 				\node (0) at (5,0.65) [draw=red,ellipse] {call};
 				\node (1) at (5,-0.65) [draw=green,ellipse] {done};
 				\path[->]
-					(0) edge (1)
-						edge [bend right] (4)
+					(0) edge [bend right] (4)
 					(2) edge (3)
 					(4) edge (5)
 					(3) edge [bend right] (1)
@@ -855,8 +862,7 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}.
 				\node (0) at (5,0.65) [draw=red,ellipse] {call};
 				\node (1) at (5,-0.65) [draw=green,ellipse] {done};
 				\path[->]
-					(0) edge (1)
-						edge [bend right] (2)
+					(0) edge [bend right] (2)
 					(2) edge (3)
 					(4) edge (5)
 					(3) edge (4)
@@ -878,8 +884,7 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}.
 				\node (0) at (7.5,0.65) [draw=red,ellipse] {call};
 				\node (1) at (7.5,-0.65) [draw=green,ellipse] {done};
 				\path[->]
-					(0) edge (1)
-						edge [bend right] (2)
+					(0)	edge [bend right] (2)
 					(2) edge (3)
 					(3) edge [bend right] (1)
 					(4) edge (5)
@@ -892,10 +897,21 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}.
 	\caption{\llccs{} interpretation as strategies}\label{fig:llccs:interp}
 \end{figure}
 
-A lot of these interpretations is what was expected: $\proc$ and $\chan$ have
-the same interpretation as presented before, $1$ is interpreted as the game
-playing \textit{done} while $0$ does not, the arrow is the type introduced for
-functions.
+In the representation above, the drawn strategies are organized in columns: for
+instance, the strategy involved in $\seman{P \parallel Q}$ has type $P^\perp
+\parallel P^\perp \parallel P$. Each column of events stands for one of those
+games, in this order.
+
+The $\seman{-}$ operator always sends a term $x_1 : A_1, \ldots, x_p : A_p
+\vdash t : B$ to a strategy $\seman{t} : \seman{A_1}^\perp \parallel \ldots
+\parallel \seman{A_p}^\perp \parallel \seman{B}$. For brevity purposes, the
+associativity and commutativity steps ---~up to isomorphism~--- will be kept
+implicit here, although those are handled very formally in the implementation.
+
+A lot of these interpretations is what was expected: $\proc$ has the same
+interpretation as presented before, and that of $\chan$ is set to the same, $1$
+is interpreted as the game playing \textit{done} while $0$ does not, the arrow
+is the type introduced for functions.
 
 A variable is represented by a \emph{copycat} of its type, to keep a version of
 the variable in the environment, reflecting the judgement $x:A \vdash x:A$.
@@ -908,21 +924,15 @@ copycat wires up perfectly $\seman{t} \parallel \seman{u}$: the version of $x$
 from the environment of $t$ is connected to $u$, and the output of $t$ is
 connected to the output of the term.
 
-In the representation above, the drawn strategies are organized in columns: for
-instance, the strategy involved in $\seman{P \parallel Q}$ has type $P^\perp
-\parallel P^\perp \parallel P$. Each column of events stands for one of those
-games, in this order.
-
-
 %%%%%%%%%%%%%%%%%%%%%
 \subsection{Adequacy}
 
-We will now prove the major result of this study, the \emph{adequacy} of the
-game semantics.
+We will now describe the main steps of the proof of the major result of this
+study, the \emph{adequacy} of the game semantics.
 
 \begin{theorem}[adequacy]
-	The previous interpretation is \emph{adequate} with the operational
-	semantics, that is
+	The previous interpretation is \emph{adequate} with respect to the
+	operational semantics, that is
 	\[ \forall P \textit{ st. } \left(\vdash P : \proc\right),~
 	\left(P \Downarrow\right) \iff \left(\seman{P} = \seman{1}\right) \]
 \end{theorem}
@@ -946,6 +956,10 @@ required.
 		\item $\forall a : \chan,~a \in l \implies \bar{a} \not\in l$.
 	\end{enumerate}
 
+	where $\freevars(P)$ denotes the set of free variables of $P$, defined as
+	usual by induction over the syntax as the set of variables unbound in the
+	term.
+
 \end{definition}
 
 \begin{lemma}
@@ -1010,7 +1024,10 @@ The theorem is mostly a consequence of the following lemma:
 	We prove its contrapositive judgement, $P \neq 1\,\&\,\seman{P} =
 	\seman{1} \implies \exists Q\,:\,P \redarrow{\tau} Q$ by induction over the
 	syntax of \linccs{} (\wlogen, we can assume that $P
-	\not\longrightarrow_\beta$, thus the terms are in \linccs): for each
+	\not\longrightarrow_\beta$, because we can always do every
+	$\beta$-reduction before any other $\tau$-reduction, and because the
+	$\beta$-reduced term corresponding to a counter-example is a
+	counter-example as well; thus the terms are in \linccs): for each
 	syntactic construction, we prove that under the induction hypotheses, there
 	is such a $Q$.
 \end{proof}
@@ -1023,10 +1040,13 @@ can compute its associated strategy and check whether it is $\seman{1}$.
 \section{Implementation of deterministic concurrent games}
 
 \hfill\href{https://tobast.fr/l3/demo.html}
-	{\includegraphics[height=2em]{tryme32.png}~\raisebox{0.5em}{Try online}}
+	{\includegraphics[height=2em]{tryme32.png}~\raisebox{0.5em}{Try
+	online\footnotemark}}
+	\footnotetext{\url{{https://tobast.fr/l3/demo.html}}}
 \qquad \href{https://github.com/tobast/cam-strategies/}
 	{\includegraphics[height=2em]{github32.png}~\raisebox{0.5em}{Github
-	repository}}
+	repository\footnotemark}}
+	\footnotetext{\url{https://github.com/tobast/cam-strategies/}}
 
 \vspace{1em}
 
@@ -1095,9 +1115,9 @@ literature.
 
 I also explored the possibility to reach a full-abstraction result. The
 full-abstraction property states that two terms are \emph{observationally
-equivalent} if and only if their (denotational) semantics are equal, that is,
-in this context,
-for all $P,Q$ two \llccs{} terms such that $\Gamma \vdash P,Q : A$,
+equivalent} if and only if their (denotational) semantics are also
+observationally equivalent, that is, in this context, for all $P,Q$ two
+\llccs{} terms such that $\Gamma \vdash P,Q : A$,
 
 \[
 	\left[ \forall \calC[-] \text{ a context }\,:\,
@@ -1105,7 +1125,14 @@ for all $P,Q$ two \llccs{} terms such that $\Gamma \vdash P,Q : A$,
 		\calC[P] \Downarrow \iff \calC[Q] \Downarrow
 		\right]
 	\quad\iff\quad
-	\left( \seman{P} = \seman{Q} \right)
+	\left( \seman{P} \simeq \seman{Q} \right)
+\]
+
+where $\simeq$ denotes the observational equivalence on strategies, that is,
+
+\[
+	(\sigma : A) \simeq (\tau : A) \iff \forall (\alpha : A^\perp \parallel
+	\proc), \alpha \strComp \sigma = \alpha \strComp \tau
 \]
 
 Yet, by lack of time, I had to abandon this path. Indeed, this would have

report/todo.sty

@@ -1,6 +1,9 @@
-\usepackage[dvipsnames]{xcolor}
+\usepackage{xcolor}
+
+\definecolor{note_text}{HTML}{671800}
+\definecolor{note_back}{HTML}{00A2E3}
 
 \newcommand{\qtodo}[1]{\colorbox{orange}{\textcolor{blue}{#1}}}
 \newcommand{\todo}[1]{\qtodo{\textbf{TODO:}\.#1}}
-\newcommand{\qnote}[1]{\colorbox{Cerulean}{\textcolor{Sepia}{[#1]}}}
+\newcommand{\qnote}[1]{\colorbox{note_back}{\textcolor{note_front}{[#1]}}}
 \newcommand{\note}[1]{\qnote{\textbf{NOTE:}\.#1}}

slides/Makefile

@@ -1,6 +1,10 @@
 TEX=slides.tex
+BASE=slides
 all: $(TEX)
 	pdflatex $(TEX)
 	pdflatex $(TEX)
 
+upload: all
+	scp $(BASE).pdf www.tobast:~/tobast.fr/public_html/l3/slides.pdf
+
 

slides/concurgames.sty

@@ -0,0 +1,63 @@
+%% By Théophile Bastian
+%% Useful commands for concurrent games as event structures
+
+\usepackage[normalem]{ulem}
+\usepackage{MnSymbol}
+\usepackage{stmaryrd}
+\usepackage{tikz}
+\usepackage{relsize}
+
+\usetikzlibrary{shapes,arrows,positioning}
+
+\newcommand{\fname}[1]{\textsc{#1}}
+
+\newcommand{\con}{\operatorname{Con}}
+\newcommand{\confl}{\raisebox{0.5em}{\uwave{\hspace{2em}}}}
+
+\newcommand{\obseq}{\simeq_\text{obs}}
+
+\newcommand{\cov}{{{\mathrel-\joinrel\subset}}}
+\newcommand{\longcov}[1]{{\stackrel{#1}
+	{\mathrel-\joinrel\relbar\joinrel\subset\,}}}
+\newcommand{\forkover}[1]{\longcov{#1}}
+\newcommand{\fork}{\cov}
+
+\newcommand{\edgeArrow}{\rightarrowtriangle}
+\newcommand{\linarrow}{\rightspoon}
+\newcommand{\redarrow}[1]{\overset{#1}{\longrightarrow}}
+
+\newcommand{\config}{\mathscr{C}}
+\newcommand{\downclose}[1]{\left[#1\right]}
+
+\newcommand{\strComp}{\odot}
+\newcommand{\strInteract}{\ostar}
+\newcommand{\strParallel}{\parallel}
+
+\newcommand{\seman}[1]{\llbracket{} #1 \rrbracket}
+
+\newcommand{\tens}{\otimes}
+\newcommand{\Tens}{\mathlarger\otimes}
+
+% LCCS
+
+\newcommand{\newch}[1]{\left(\nu #1\right)}
+
+\newcommand{\linearmark}{$\mathcal{L}$}
+\newcommand{\lcalc}{$\lambda$-calculus}
+\newcommand{\lccs}{$\lambda$CCS}
+\newcommand{\linccs}{{\linearmark}CCS}
+\newcommand{\llccs}{$\lambda${\linearmark}CCS}
+\newcommand{\proc}{\mathbb{P}}
+\newcommand{\chan}{\mathbb{C}}
+
+\newcommand{\validctx}{\mathcal{L}}
+\newcommand{\freevars}{\operatorname{fv}}
+
+% Copycat
+\newcommand{\CC}{{\rm C\!\!\!C}}
+\newcommand{\cc}{\mathrm{\,c\!\!\!\!c\,}}
+
+\newcommand{\includedot}[2][]{%
+	\begin{tikzpicture}[>=latex,line join=bevel,#1]
+	\input{_build/dot/#2.tex}
+	\end{tikzpicture}}

slides/math.sty

@@ -0,0 +1,80 @@
+\usepackage{stmaryrd}
+\usepackage{amsmath}
+\usepackage{amsfonts}
+\usepackage{amssymb}
+\usepackage{amsthm}
+\usepackage{mathtools}
+\usepackage{fancybox}
+\usepackage{mathrsfs}
+\usepackage{mathtools}
+
+\newcommand{\eqdef}{{~\coloneqq~}}
+\newcommand{\lAnd}{~\&~}
+
+\newcommand{\overOr}[2]{\begin{array}{r l}
+	& #1 \\
+	\textit{or} & \\
+	& #2
+\end{array}}
+
+\newcommand{\id}{\operatorname{id}}
+
+% Intervalle discret.
+\newcommand{\discrIv}[1]{\llbracket #1 \rrbracket}
+
+% ensembliste
+\newcommand{\set}[1]{\left\{ #1 \right\}}
+\newcommand{\card}[1]{\left\vert{} #1 \right\vert}
+\newcommand{\abs}[1]{\left\vert{} #1 \right\vert}
+\newcommand{\interior}[1]{\left({#1}\right)^\circ}
+\newcommand{\floor}[1]{\left\lfloor{} #1 \right\rfloor}
+\newcommand{\ceil}[1]{\left\lceil{} #1 \right\rceil}
+
+% Abréviations courrantes
+\newcommand{\ie}{\textit{ie.}}
+\newcommand{\eg}{\textit{eg.}}
+\newcommand{\Eg}{\textit{Eg.}}
+\newcommand{\wrt}{\textit{wrt.}}
+\newcommand{\wlogen}{\textit{wlog.}}
+\newcommand{\st}{\textit{st.}}
+
+% Notations à polices étranges
+\newcommand{\domain}{\mathcal{D}}
+\newcommand{\bigO}{\mathcal{O}}
+\newcommand{\calA}{\mathcal{A}}
+\newcommand{\calC}{\mathcal{C}}
+\newcommand{\calG}{\mathcal{G}}
+\newcommand{\calV}{\mathcal{V}}
+\newcommand{\calT}{\mathcal{T}}
+\newcommand{\calP}{\mathcal{P}}
+
+% Ensembles
+\newcommand{\realset}{\mathbb{R}}
+\newcommand{\natset}{\mathbb{N}}
+\newcommand{\relset}{\mathbb{Z}}
+
+% Probas
+\newcommand{\prob}{\mathbb{P}}
+\newcommand{\probP}[1]{\mathbb{P}\left(#1\right)}
+\newcommand{\expec}{\mathbb{E}}
+\newcommand{\expecP}[1]{\mathbb{E}\left[#1\right]}
+\newcommand{\variance}{\mathbb{V}}
+\newcommand{\ber}{\mathcal{B}er}
+\newcommand{\bin}{\mathcal{B}in}
+\newcommand{\poi}{\mathcal{P}oi}
+
+% Suppression des points
+\newcommand{\ibar}{\overline{\imath}}
+\newcommand{\jbar}{\overline{\jmath}}
+
+% Fonctions
+%\newcommand{\functiondef}[4]{\left\lbrace \begin{tabular}{r l} #1 & \rightarrow #2 \\ #3 & \mapsto #4\end{tabular} \right.}
+\newcommand{\functiondef}[4]{\begin{cases}
+#1 & \to #2 \\
+#3 & \mapsto #4
+\end{cases}}
+
+
+% Preuve par équivalence - puces
+\newcommand{\impliesbullet}{\ovalbox{$\implies$}}
+\newcommand{\impliedbybullet}{\ovalbox{$\impliedby$}}

slides/my_hyperref.sty

@@ -0,0 +1,26 @@
+\usepackage{hyperref}
+\usepackage{xcolor}
+
+\definecolor{link_blue}{RGB}{0,0,97}
+\definecolor{cite_green}{HTML}{009B55}
+
+\hypersetup{
+%    bookmarks=true,         % show bookmarks bar?
+%    unicode=false,          % non-Latin characters in Acrobat’s bookmarks
+%    pdftoolbar=true,        % show Acrobat’s toolbar?
+%    pdfmenubar=true,        % show Acrobat’s menu?
+%    pdffitwindow=false,     % window fit to page when opened
+%    pdfstartview={FitH},    % fits the width of the page to the window
+%    pdftitle={My title},    % title
+%    pdfauthor={Author},     % author
+%    pdfsubject={Subject},   % subject of the document
+%    pdfcreator={Creator},   % creator of the document
+%    pdfproducer={Producer}, % producer of the document
+%    pdfkeywords={keyword1} {key2} {key3}, % list of keywords
+%    pdfnewwindow=true,      % links in new PDF window
+    colorlinks=true,       % false: boxed links; true: colored links
+    linkcolor=link_blue,          % color of internal links (change box color with linkbordercolor)
+    citecolor=cite_green,        % color of links to bibliography
+    filecolor=magenta,      % color of file links
+    urlcolor=link_blue           % color of external links
+}

slides/my_listings.sty

@@ -0,0 +1,63 @@
+\usepackage{listings}
+\usepackage{algorithmicx}
+\usepackage{algpseudocode}
+\usepackage{color}
+\usepackage{xcolor}
+\usepackage{courier}
+\definecolor{color_comment}{HTML}{2D6F19}
+\definecolor{color_linenum}{HTML}{9E9E9E}
+\definecolor{color_strings}{HTML}{D300F3}
+
+
+\lstset{ %
+%	backgroundcolor=\color{white},   % choose the background color; you must add \usepackage{color} or \usepackage{xcolor}
+	basicstyle=\footnotesize\ttfamily,	% the size of the fonts that are used for the code
+	breakatwhitespace=false,         % sets if automatic breaks should only happen at whitespace
+	breaklines=true,                 % sets automatic line breaking
+	captionpos=b,                    % sets the caption-position to bottom
+	commentstyle=\color{color_comment},    % comment style
+%	deletekeywords={...},            % if you want to delete keywords from the given language
+%	escapeinside={\%*}{*)},          % if you want to add LaTeX within your code
+	extendedchars=true,              % lets you use non-ASCII characters; for 8-bits encodings only, does not work with UTF-8
+	frame=none,                         % adds a frame around the code
+	keepspaces=true,                 % keeps spaces in text, useful for keeping indentation of code (possibly needs columns=flexible)
+	keywordstyle=\color{blue},       % keyword style
+	morekeywords={*,...},            % if you want to add more keywords to the set
+	numbers=left,                    % where to put the line-numbers; possible values are (none, left, right)
+	numbersep=5pt,                   % how far the line-numbers are from the code
+	numberstyle=\tiny\color{color_linenum}, % the style that is used for the line-numbers
+	rulecolor=\color{black},         % if not set, the frame-color may be changed on line-breaks within not-black text (e.g. comments (green here))
+	showspaces=false,                % show spaces everywhere adding particular underscores; it overrides 'showstringspaces'
+	showstringspaces=false,          % underline spaces within strings only
+	showtabs=false,                  % show tabs within strings adding particular underscores
+	stepnumber=1,                    % the step between two line-numbers. If it's 1, each line will be numbered
+	stringstyle=\color{color_strings},  % string literal style
+	tabsize=4,                       % sets default tabsize to 2 spaces
+%	title=\lstname,                  % show the filename of files included with \lstinputlisting; also try caption instead of title
+%	inputencoding=utf8/latin1        % To accept utf8 encoding
+}
+
+\lstset{literate=
+	{á}{{\'a}}1 {é}{{\'e}}1 {í}{{\'i}}1 {ó}{{\'o}}1 {ú}{{\'u}}1
+	{Á}{{\'A}}1 {É}{{\'E}}1 {Í}{{\'I}}1 {Ó}{{\'O}}1 {Ú}{{\'U}}1
+	{à}{{\`a}}1 {è}{{\`e}}1 {ì}{{\`i}}1 {ò}{{\`o}}1 {ù}{{\`u}}1
+	{À}{{\`A}}1 {È}{{\'E}}1 {Ì}{{\`I}}1 {Ò}{{\`O}}1 {Ù}{{\`U}}1
+	{ä}{{\"a}}1 {ë}{{\"e}}1 {ï}{{\"i}}1 {ö}{{\"o}}1 {ü}{{\"u}}1
+	{Ä}{{\"A}}1 {Ë}{{\"E}}1 {Ï}{{\"I}}1 {Ö}{{\"O}}1 {Ü}{{\"U}}1
+	{â}{{\^a}}1 {ê}{{\^e}}1 {î}{{\^i}}1 {ô}{{\^o}}1 {û}{{\^u}}1
+	{Â}{{\^A}}1 {Ê}{{\^E}}1 {Î}{{\^I}}1 {Ô}{{\^O}}1 {Û}{{\^U}}1
+	{œ}{{\oe}}1 {Œ}{{\OE}}1 {æ}{{\ae}}1 {Æ}{{\AE}}1 {ß}{{\ss}}1
+	{ű}{{\H{u}}}1 {Ű}{{\H{U}}}1 {ő}{{\H{o}}}1 {Ő}{{\H{O}}}1
+	{ç}{{\c c}}1 {Ç}{{\c C}}1 {ø}{{\o}}1 {å}{{\r a}}1 {Å}{{\r A}}1
+	{€}{{\EUR}}1 {£}{{\pounds}}1 {¬}{{$\lnot$}}1 {∞}{{$\infty$}}1	
+}
+
+\newcommand{\true}{\lstinline$true$}
+\newcommand{\false}{\lstinline$false$}
+
+\newcommand{\lstbash}[1]{\lstinline[language=bash]$#1$}
+\newcommand{\lstocaml}[1]{\lstinline[language=Caml]$#1$}
+\newcommand{\lstcpp}[1]{\lstinline[language=C++]$#1$}
+\newcommand{\lstc}[1]{\lstinline[language=C]$#1$}
+\newcommand{\lstpython}[1]{\lstinline[language=python]$#1$}
+

slides/slides.tex

@@ -1,36 +1,397 @@
+% vim: :spell spelllang=fr
 \documentclass[11pt]{beamer}
 \usetheme{Warsaw}
+%\usecolortheme{wolverine}
 \usepackage[utf8]{inputenc}
 \usepackage[french]{babel}
 \usepackage[T1]{fontenc}
+%\usepackage{my_hyperref}
+\usepackage{my_listings}
+\usepackage{libertine}
 \usepackage{amsmath}
 \usepackage{amsfonts}
 \usepackage{amssymb}
 \usepackage{graphicx}
-\usepackage{my_listings}
-\usepackage{my_hyperref}
+\usepackage{concurgames}
+\usepackage{theorems}
+\usepackage{todo}
 \usepackage{math}
+\usepackage{tikz}
+
+\usetikzlibrary{positioning}
+
 \setbeamertemplate{navigation symbols}{}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\author{Théophile \textsc{Bastian}\\
+\author[Théophile \textsc{Bastian}]{Théophile \textsc{Bastian}\\
 \small{Sous la supervision de Glynn \textsc{Winskel} et Pierre
 \textsc{Clairambault}}}
-\title{Soutenance de stage\\
-Structures d'événements dans la sémantique des jeux}
-\date{Juin\,--\,Juillet 2016}
+\title{Soutenance de stage}
+%\subtitle{Structures d'événements dans la sémantique des jeux}
+\subtitle{Sémantique déterministe de langage concurrentiel en sémantique des
+jeux}
+\date{Juin\,--\,juillet 2016}
 %\logo{}
 \institute{Computer Laboratory --- Cambridge, UK}
 \begin{document}
 
 \begin{frame}
 	\titlepage{}
+%	\tableofcontents
+\end{frame}
+
+\begin{frame}
 	\tableofcontents
 \end{frame}
 
-%\begin{frame}
-%\tableofcontents
-%\end{frame}
+\section{Langage étudié}
+
+\begin{frame}{\llccs~: syntaxe}
+	\begin{columns}[t]
+		\column{0.5\textwidth}
+		\begin{center}Termes\end{center}\vspace{-1em}
+		\begin{align*}
+			t,u,\ldots ::=~&1 & \text{(succès)}\\
+			\vert~&0 & \text{(erreur)}\\
+			\vert~&t \parallel u & \text{(parallèle)}\\
+			\vert~&t \cdot u & \text{(séquentiel)}\\
+			\vert~&(\nu a) t & \text{(nouveau canal)} \\
+			& & \\
+			\vert~&x \in \mathbb{V} & \text{(variable)} \\
+			\vert~&t\,u & \text{(application)}\\
+			\vert~&\lambda x^A \cdot t & \text{(abstraction)}\\
+		\end{align*}
+		\column{0.5\textwidth}
+		\begin{center}Types\end{center}\vspace{-1em}
+		\begin{align*}
+			A,B,\ldots ::=~&\proc & \text{(processus)} \\
+			\vert~&\chan & \text{(canal)} \\
+			\vert~&A \linarrow B & \text{(flèche linéaire)}
+		\end{align*}
+	\end{columns}
+\end{frame}
+
+\begin{frame}{\llccs~: règles de typage}
+	\begin{align*}
+		\frac{~}{\,\vdash 0:\proc} & (\textit{Ax}_0) &
+		\frac{~}{\,\vdash 1:\proc} & (\textit{Ax}_1) &
+		\alert{\frac{~}{t:A \vdash t:A}} & \alert{(\textit{Ax})} &
+	\end{align*}\vspace{-1em}\begin{align*}
+		\frac{\Gamma \vdash P : \proc \quad \Delta \vdash Q : \proc}
+			{\Gamma,\Delta \vdash P \cdot Q : \proc}
+			& (\cdot_\proc) &
+		\frac{\Gamma \vdash P : \proc}
+			{\Gamma,a:\chan \vdash a \cdot P: \proc}
+			& (\cdot_\chan)
+	\end{align*} \vspace{-1em} \begin{align*}
+		\alert{\frac{\Gamma \vdash P : \proc \quad \Delta \vdash Q : \proc}
+			{\Gamma,\Delta \vdash P \parallel Q : \proc}}
+			& \alert{(\parallel)} &
+		\frac{\Gamma, a:\chan, \bar{a}:\chan \vdash P : \proc}
+			{\Gamma \vdash (\nu a) P : \proc}
+			& (\nu)
+	\end{align*}
+
+	\begin{align*}
+		\frac{~}{x : A \vdash x : A} & (\textit{Ax}) &
+		\frac{\Gamma \vdash t : A \linarrow B \quad \Delta \vdash u : A}
+			{\Gamma,\Delta \vdash t~u : B} & (\textit{App}) &
+	\end{align*} \vspace{-1em} \begin{align*}
+		\frac{\Gamma, x : A \vdash t : B}
+			{\Gamma \vdash \lambda x^{A} \cdot t : A \linarrow B} & (Abs)
+	\end{align*}
+\end{frame}
+
+\begin{frame}{\llccs~: sémantique opérationnelle}
+	\begin{align*}
+		\frac{~}{a \cdot P \redarrow{a} P} & &
+		\frac{~}{1 \parallel P \redarrow{\tau} P} & &
+		\frac{~}{1 \cdot P \redarrow{\tau} P} & &
+	\end{align*}\begin{align*}
+		\frac{P \longrightarrow_\beta Q}
+			{P \redarrow{\tau} Q} & &
+		\frac{P \redarrow{\tau_c} Q}
+			{(\nu a) P \redarrow{\tau} Q} & (c \in \set{a,\bar{a}})&
+	\end{align*}\begin{align*}
+		\alert{\frac{P \redarrow{a} P'\quad Q \redarrow{\bar{a}} Q'}
+			{P \parallel Q \redarrow{\tau_a} P' \parallel Q'}} & &
+		\frac{P \redarrow{x} P'}
+			{(\nu a)P \redarrow{x} (\nu a)P'} & (x \not\in \set{a,\tau_a}) &
+	\end{align*}\begin{align*}
+		\frac{P \redarrow{x} P'}
+			{P \parallel Q \redarrow{x} P' \parallel Q} & &
+		\frac{Q \redarrow{x} Q'}
+			{P \parallel Q \redarrow{x} P \parallel Q'} & &
+		\frac{P \redarrow{x} P'}
+			{P \cdot Q \redarrow{x} P' \cdot Q} & &
+	\end{align*}
+\end{frame}
+
+\begin{frame}{Quelques exemples}
+	\begin{itemize}
+		\item $(1 \parallel 1) \cdot 1$~: succès
+			\pause%
+		\item $\newch{a} (a \cdot 1 \parallel \bar{a} \cdot 1)$
+			\pause%
+		\item $\newch{a} (a \cdot \bar{a} \cdot 1)$~: \textit{deadlock}
+			\pause%
+		\item $F := \lambda x^\chan \cdot \lambda y^\chan \cdot x \cdot y \cdot
+			1$
+			\pause%
+		\item $\newch{a} F\,a\,\bar{a}$~: \textit{deadlock}
+			\pause%
+		\item $\newch{a} \newch{b} (F\,a\,b \parallel \bar{a} \cdot \bar{b}
+			\cdot 1)$~: termine
+	\end{itemize}
+\end{frame}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Structures d'événements}
+
+\begin{frame}{Sémantique des jeux}
+	\begin{itemize}
+		\item Programme $\longrightarrow$ jeu à deux joueurs
+		\pause\vspace{1em}
+		\item \textit{Player}~: joue pour le programme
+		\item \textit{Opponent}~: joue pour l'environnement (OS, utilisateur,
+			\ldots)
+		\pause\vspace{1em}
+		\item \textit{Jeu}~: structure imposée (architecture physique, \ldots)
+		\item \textit{Stratégie}~: modélisation du programme
+	\end{itemize}
+\end{frame}
+
+\subsection{Sémantique par entrelacements}
+
+\begin{frame}{Sémantique usuelle~: par entrelacements}
+	\begin{itemize}
+		\item Jeux en arbres\\
+			\begin{columns}
+				\column{0.5\textwidth}
+				\begin{center}\begin{tikzpicture}[node distance=0.5cm]
+					\node (1) {a};
+					\node (2) [below left=of 1] {b};
+					\node (3) [below right=of 1] {c};
+					\path [->]
+						(1) edge (2)
+							edge (3);
+				\end{tikzpicture}
+				\end{center}
+
+				\column{0.5\textwidth}
+				États du jeu~: $\varepsilon,~a,~a \cdot b,~a \cdot c$
+			\end{columns}
+
+		\pause%
+		\item \og{}Exécution parallèle~\fg{}:
+			\begin{columns}
+				\column{0.5\textwidth}
+				\begin{center}\begin{tikzpicture}[node distance=0.5cm]
+					\node (1) {a};
+					\node (2) [below left=of 1] {b};
+					\node (3) [below right=of 1] {c};
+					\node (5) [right=of 3] {e};
+					\node (4) [above right=of 5] {d};
+					\node (6) [below right=of 4] {f};
+					\path [->]
+						(1) edge (2)
+							edge (3)
+						(4) edge (5)
+							edge (6);
+				\end{tikzpicture}
+				\end{center}
+
+				\column{0.5\textwidth}
+				États du jeu~: $\varepsilon,~a,~d,~a \cdot b,~a \cdot d \cdot e
+				\cdot b, \ldots$
+			\end{columns}
+
+		\pause%
+		\item Comment représenter \og{}proprement~\fg{} le jeu suivant~?
+			\begin{center}\begin{tikzpicture}[node distance=0.5cm]
+				\node (3) {c};
+				\node (1) [above left=of 3] {a};
+				\node (2) [above right=of 3] {b};
+				\path [->]
+					(1) edge (3)
+					(2) edge (3);
+			\end{tikzpicture}
+			\end{center}
+
+	\end{itemize}
+\end{frame}
+
+\subsection{Structures d'événements}
+
+\begin{frame}{Structures d'événements}
+	\begin{definition}{structure d'événement (déterministe)}
+		$(E, \leq_E)$ ensemble d'\emph{événements} partiellement ordonné.
+	\end{definition}
+	\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}$.
+
+		$E^\perp$~: SEP $E$ avec $\rho^\perp$.
+	\end{definition}
+	$\qquad\longrightarrow$ DAG
+	\pause%
+	\begin{definition}{configuration}
+		$x \subseteq E$ tel que $\forall e \in E, e' \in x, e \leq e' \implies
+		e \in x$.\\
+		$\config(E)$~: ensemble des configurations de $E$.\\
+		Pour $e \in E$, $[e]$ configuration induite par $e$.
+	\end{definition}
+\end{frame}
+
+\begin{frame}{Structures d'événements (suite)}
+	\begin{definition}{stratégie}
+		$\left(\sigma : A\right)$~: stratégie sur $A$ si $\sigma$ SEP
+		\textit{tq.}\\
+		\begin{itemize}
+			\item $\sigma \subseteq A$
+			\item $\config(\sigma) \subseteq \config(A)$
+			\item $\rho_\sigma = {\rho_A}_{\vert \sigma}$
+			\item $\cc_A \strComp \sigma = \sigma$ ($\cc_A$~:
+				\og{}identité~\fg)
+		\end{itemize}
+	\end{definition}
+\end{frame}
+
+\begin{frame}{Opérations sur structures d'événements}
+	\begin{definition}{parallèle}
+		$A \parallel B := \set{0} \times A \cup \set{1} \times B$~: mise
+		en parallèle de deux SE\@.
+	\end{definition}
+
+	\begin{definition}{interaction}
+		Pour $\sigma : A$, $\tau : A^\perp$, $\sigma \wedge \tau$~: $\sigma
+		\cap \tau$ où les boucles causales sont retirées.
+	\end{definition}
+
+	\begin{definition}{composition}
+		Pour $\sigma : A^\perp \parallel B$, $\tau : B^\perp \parallel C$,
+		\[ \tau \strComp \sigma := \left(\sigma \parallel C^\perp\right) \wedge
+			\left(A \parallel \tau\right) \]
+	\end{definition}
+
+	\begin{definition}{copycat}
+		$\cc_A : A^\perp \parallel A$~: $(A^\perp \parallel \emptyset) \cup
+		(\emptyset \parallel A)$, plus les $\ominus \rightarrow \oplus$ d'une
+		composante à l'autre.
+	\end{definition}
+\end{frame}
+
+
+\section{Interprétation de \llccs}
+
+\subsection{Sémantique dénotationnelle}
+
+\begin{frame}{Interprétation de \llccs}
+	\begin{columns}[c]
+		\column{0.5\textwidth}
+
+		\begin{align*}
+			\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}
+		\begin{align*}
+			\seman{x^A} &\eqdef \cc_{\seman{A}} \\
+			\seman{A \linarrow B} &\eqdef \seman{A}^\perp \parallel \seman{B}\\
+			\seman{t^{A \linarrow B}~u^{A}} &\eqdef
+				\cc_{A \linarrow B} \strComp \left( \seman{t} \parallel
+				\seman{u} \right) \\
+			\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}
 

slides/theorems.sty

@@ -0,0 +1,5 @@
+% vim: :spell spelllang=fr
+
+\renewenvironment{definition}[1]{\begin{block}{Définition~: #1.}}{\end{block}}
+\renewenvironment{theorem}[1]{\begin{alertblock}{Théorème~: #1.}}{\end{alertblock}}
+\renewenvironment{lemma}[1]{\begin{block}{Lemme~: #1.}}{\end{block}}

slides/todo.sty

@@ -0,0 +1,9 @@
+\usepackage{xcolor}
+
+\definecolor{note_text}{HTML}{671800}
+\definecolor{note_back}{HTML}{00A2E3}
+
+\newcommand{\qtodo}[1]{\colorbox{orange}{\textcolor{blue}{#1}}}
+\newcommand{\todo}[1]{\qtodo{\textbf{TODO:}\.#1}}
+\newcommand{\qnote}[1]{\colorbox{note_back}{\textcolor{note_front}{[#1]}}}
+\renewcommand{\note}[1]{\qnote{\textbf{NOTE:}\.#1}}