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,8 +1,7 @@
 \usepackage{hyperref}
-\usepackage{xcolor}
+\usepackage[dvipsnames]{xcolor}
 
 \definecolor{link_blue}{RGB}{0,0,97}
-\definecolor{cite_green}{HTML}{009B55}
 
 \hypersetup{
 %    bookmarks=true,         % show bookmarks bar?
@@ -20,7 +19,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=cite_green,        % color of links to bibliography
+    citecolor=ForestGreen,        % color of links to bibliography
     filecolor=magenta,      % color of file links
     urlcolor=link_blue           % color of external links
 }

report/report.tex

@@ -83,13 +83,14 @@ 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 first tackled by
+focus at some point on modelling concurrency. The problem was 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. \fname{Ghica} and \fname{Murawski} then simplified
+communication on channels. It is often considered, though, that \fname{Ghica}
-\textsc{Laird}'s approach, and gave a fully abstract model for a slightly more
+and \fname{Murawski}~\cite{ghica2004angelic} really took the fundamental step
-realistic concurrent programming language with shared memory
+by defining game semantics for a fine-grained concurrent language including
-in~\cite{ghica2004angelic}.
+parallel execution of ``threads'' and low-level semaphores --- a way more
+realistic approach to the problem.
 
 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
@@ -104,15 +105,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, even for concurrent programs it is
+non-deterministic uniform choice. Yet, one could reasonably argue that a
-often a desirable property that they should behave consistently with the
+program should behave consistently with the environment, which would mean that
-environment, meaning that they are deterministic up to the choice of the
+the semantics of a program --- even a concurrent one --- should still be
-scheduler.  Such determinism can be ensured statically, via typing. This idea
+deterministic. This idea was explored outside of the game semantics context,
-was explored outside of the game semantics context, for instance
+for instance by~\cite{reynolds1978syntactic}, establishing a type-checking
-by~\cite{reynolds1978syntactic}, establishing a type-checking system to
+system to restrict concurrent programs to deterministic ones. Some recent work
-restrict concurrent programs to deterministic ones. Some recent work makes use
+makes use of linear logic~\cite{caires2010session} for similar purposes as
-of linear logic~\cite{caires2010session} for similar purposes as well.  Yet,
+well.  Yet, the interleavings game semantics of these languages remains
-the interleavings game semantics of these languages remains non-deterministic.
+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
@@ -141,7 +142,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 through the banning of interference.
+determinism requirements.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \subsection{A linear variant of CCS~: \linccs}
@@ -230,7 +231,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'} & (x \not\in \set{a,\tau_a})
+			{(\nu a)P \redarrow{x} (\nu a)P'} & (a \not\in \set{x,\tau_a})
 	\end{align*}
 	\caption{\linccs{} operational semantics}\label{fig:lccs:opsem}
 \end{figure}
@@ -244,7 +245,11 @@ 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 for $\tau$-reductions.
+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.
 
 \subsection{Lifting to the higher order: linear \lcalc}
 
@@ -252,7 +257,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).
+the typing rules). In particular, the only base types are $\proc$ and $\chan$.
 
 \begin{figure}[h]
 	\begin{minipage}[t]{0.55\textwidth}
@@ -333,17 +338,15 @@ 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, that is, its declaration ignores duality
+		channels are dual or not.
-		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 deterministic games model for the above language. For
+Our goal is now to give a games model for the above language. For that purpose,
-that purpose, we will use \emph{event structures}, providing an alternative
+we will use \emph{event structures}, providing an alternative formalism to
-formalism to the often-used tree-like games.
+the often-used tree-like games.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \subsection{The event structures framework}
@@ -368,9 +371,9 @@ corresponds to the game tree
 \]
 
 This can of course be used to describe much larger games, and is often useful
-to reason concurrently. The different configurations of the game that can be
+to reason concurrently, since the causal histories appears clearly: the
-reached are quite easily read: one only has to concatenate the events found
+possible states of the game can be read easily by concatenating the events
-along path starting at the root of the tree.
+found along a path from 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
@@ -392,14 +395,10 @@ before Player can play $C$. The corresponding tree-like game would be
 	\end{tikzpicture}
 \]
 
-This goes even worse with less structure: since there are $n!$ % chktex 40
+This goes even worse with less structure: since there is $n!$ % chktex 40
 permutations for $n$ elements, the tree can grow way larger.
 
-The previous example also points out a kind of \textit{obfuscation} of the
+This problem motivated the use of \emph{event structures} as a formalism to
-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.
@@ -434,9 +433,7 @@ 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$, \ie{} the
+	over $E$ that is defined as the transitive reduction of $\leq_E$.
-	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
@@ -445,7 +442,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$ (\ie{} $\edgeArrow_E$).
+reduction of $\leq_E$.
 
 \begin{definition}[event structure with polarities]
 	An \emph{event structure with polarities} (\textit{ESP}) is an event
@@ -488,9 +485,8 @@ 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$
-	is used to mean that the standard union ($\cup$) is disjoint. It is also
+	denotes the disjoint union. It is also possible to write $x \forkover{e}$,
-	possible to write $x \forkover{e}$, stating that $x \sqcup \set{e} \in
+	stating that $x \sqcup \set{e} \in \config(A)$, or $x \fork y$.
-	\config(A)$, or $x \fork y$.
 \end{notation}
 
 %%%%%
@@ -538,7 +534,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 $\texttt{call} \leq \texttt{done}$
+	finished, if it ever does. The relation $\text{call} \leq \text{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.
@@ -548,8 +544,7 @@ drink.
 	A \emph{pre-strategy} on the game $A$, written $\sigma: A$, is an ESP such
 	that
 	\begin{enumerate}[(i)]
-		\item $\sigma \subseteq A$ (inclusion over set of events, not including
+		\item $\sigma \subseteq A$;
-			the order);
 		\item $\config(\sigma) \subseteq \config(A)$;
 		\item $\forall s \in \sigma, \rho_A(s) = \rho_\sigma(s)$
 	\end{enumerate}
@@ -605,26 +600,23 @@ 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 a variant of the above strategy would be
+$\text{call}_0 \leq \text{call}_1$ on the above strategy is allowed, stating
-allowed, stating that the operating system cannot decide to start the process
+that the operating system cannot decide to start the process $1$ before the
-$1$ before the process $0$. It is not up to the program to decide that, this
+process $0$. It is not up to the program to decide that, this strategy is thus
-strategy is thus unrealistic. We then have to restrict pre-strategies to
+unrealistic. We then have to restrict pre-strategies to \emph{strategies}:
-\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}: $\forall x \in \config(\sigma), x \sqcup
+			\textit{receptive}: for all $x \in \config(A)$ \st{}
-			\set{e} \in \config(A) \land \rho(e) = \ominus \implies x \sqcup
+			$x \forkover{e^-}$, $e \in \sigma$;
-			\set{e} \in \config(\sigma)$
-
 
 		\item\label{def:courteous}
-			\textit{courteous}: $\forall e \edgeArrow_\sigma e' \in \sigma$,
+			\textit{courteous}: $\forall x \edgeArrow_\sigma x' \in \sigma$,
-			$(\rho(e),\rho(e')) \neq (-,+) \implies
+			$(\rho(x),\rho(x')) \neq (-,+) \implies
-			e \edgeArrow_A e'$.
+			x \edgeArrow_A x'$.
 	\end{enumerate}
 \end{definition}
 
@@ -642,8 +634,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
-$e$ then $e'$, it is undefined whether Opponent will receive $e$ then $e'$ or
+$x$ then $y$, it is undefined whether Opponent will receive $x$ then $y$ or $y$
-$e'$ then $e$.
+then $x$.
 
 %%%%%
 \subsubsection{Operations on games and strategies}\label{sssec:es_operations}
@@ -688,7 +680,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 partial order.
+	contained in such loops from $\sigma \cap \tau$, yielding a regular order.
 \end{definition}
 
 \textit{This construction is a simplified version of the analogous one
@@ -715,8 +707,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^\perp) \wedge
+	\sigma$ is an event structure defined as $(\sigma \parallel C) \wedge
-	(A \parallel \tau)$, where $A$ and $C^\perp$ are seen as strategies.
+	(A^\perp \parallel \tau)$, where $A^\perp$ and $C$ are seen as strategies.
 \end{definition}
 
 The idea is to put in correspondence the ``middle'' states (those of $B$) while
@@ -754,8 +746,7 @@ 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 : A$, $\sigma$ is a strategy $\iff$ $\cc_A \strComp \sigma = \sigma$.
-\sigma$~\cite{rideau2011concurrent}.
 
 \begin{example}[copycat]
 	If we consider the following game $A$
@@ -817,7 +808,8 @@ 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 [bend right] (2)
+					(0) edge (1)
+						edge [bend right] (2)
 						edge [bend right] (4)
 					(2) edge (3)
 					(4) edge (5)
@@ -840,7 +832,8 @@ 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 [bend right] (4)
+					(0) edge (1)
+						edge [bend right] (4)
 					(2) edge (3)
 					(4) edge (5)
 					(3) edge [bend right] (1)
@@ -862,7 +855,8 @@ 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 [bend right] (2)
+					(0) edge (1)
+						edge [bend right] (2)
 					(2) edge (3)
 					(4) edge (5)
 					(3) edge (4)
@@ -884,7 +878,8 @@ 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 [bend right] (2)
+					(0) edge (1)
+						edge [bend right] (2)
 					(2) edge (3)
 					(3) edge [bend right] (1)
 					(4) edge (5)
@@ -897,21 +892,10 @@ language as strategies as defined in figure~\ref{fig:llccs:interp}.
 	\caption{\llccs{} interpretation as strategies}\label{fig:llccs:interp}
 \end{figure}
 
-In the representation above, the drawn strategies are organized in columns: for
+A lot of these interpretations is what was expected: $\proc$ and $\chan$ have
-instance, the strategy involved in $\seman{P \parallel Q}$ has type $P^\perp
+the same interpretation as presented before, $1$ is interpreted as the game
-\parallel P^\perp \parallel P$. Each column of events stands for one of those
+playing \textit{done} while $0$ does not, the arrow is the type introduced for
-games, in this order.
+functions.
-
-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$.
@@ -924,15 +908,21 @@ 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 describe the main steps of the proof of the major result of this
+We will now prove the major result of this study, the \emph{adequacy} of the
-study, the \emph{adequacy} of the game semantics.
+game semantics.
 
 \begin{theorem}[adequacy]
-	The previous interpretation is \emph{adequate} with respect to the
+	The previous interpretation is \emph{adequate} with the operational
-	operational semantics, that is
+	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}
@@ -956,10 +946,6 @@ 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}
@@ -1024,10 +1010,7 @@ 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$, because we can always do every
+	\not\longrightarrow_\beta$, thus the terms are in \linccs): for each
-	$\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}
@@ -1040,13 +1023,10 @@ 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
+	{\includegraphics[height=2em]{tryme32.png}~\raisebox{0.5em}{Try online}}
-	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\footnotemark}}
+	repository}}
-	\footnotetext{\url{https://github.com/tobast/cam-strategies/}}
 
 \vspace{1em}
 
@@ -1115,9 +1095,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 also
+equivalent} if and only if their (denotational) semantics are equal, that is,
-observationally equivalent, that is, in this context, for all $P,Q$ two
+in this context,
-\llccs{} terms such that $\Gamma \vdash P,Q : A$,
+for all $P,Q$ two \llccs{} terms such that $\Gamma \vdash P,Q : A$,
 
 \[
 	\left[ \forall \calC[-] \text{ a context }\,:\,
@@ -1125,14 +1105,7 @@ observationally equivalent, that is, in this context, for all $P,Q$ two
 		\calC[P] \Downarrow \iff \calC[Q] \Downarrow
 		\right]
 	\quad\iff\quad
-	\left( \seman{P} \simeq \seman{Q} \right)
+	\left( \seman{P} = \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,9 +1,6 @@
-\usepackage{xcolor}
+\usepackage[dvipsnames]{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]}}}
+\newcommand{\qnote}[1]{\colorbox{Cerulean}{\textcolor{Sepia}{[#1]}}}
 \newcommand{\note}[1]{\qnote{\textbf{NOTE:}\.#1}}

slides/Makefile

@@ -1,10 +1,6 @@
 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

@@ -1,63 +0,0 @@
-%% 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

@@ -1,80 +0,0 @@
-\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

@@ -1,26 +0,0 @@
-\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

@@ -1,63 +0,0 @@
-\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,397 +1,36 @@
-% 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{concurgames}
+\usepackage{my_listings}
-\usepackage{theorems}
+\usepackage{my_hyperref}
-\usepackage{todo}
 \usepackage{math}
-\usepackage{tikz}
-
-\usetikzlibrary{positioning}
-
 \setbeamertemplate{navigation symbols}{}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\author[Théophile \textsc{Bastian}]{Théophile \textsc{Bastian}\\
+\author{Théophile \textsc{Bastian}\\
 \small{Sous la supervision de Glynn \textsc{Winskel} et Pierre
 \textsc{Clairambault}}}
-\title{Soutenance de stage}
+\title{Soutenance de stage\\
-%\subtitle{Structures d'événements dans la sémantique des jeux}
+Structures d'événements dans la sémantique des jeux}
-\subtitle{Sémantique déterministe de langage concurrentiel en sémantique des
+\date{Juin\,--\,Juillet 2016}
-jeux}
-\date{Juin\,--\,juillet 2016}
 %\logo{}
 \institute{Computer Laboratory --- Cambridge, UK}
 \begin{document}
 
 \begin{frame}
 	\titlepage{}
-%	\tableofcontents
-\end{frame}
-
-\begin{frame}
 	\tableofcontents
 \end{frame}
 
-\section{Langage étudié}
+%\begin{frame}
-
+%\tableofcontents
-\begin{frame}{\llccs~: syntaxe}
+%\end{frame}
-	\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

@@ -1,5 +0,0 @@
-% 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

@@ -1,9 +0,0 @@
-\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}}