diff --git a/biblio.bib b/biblio.bib
index dced266..ebad511 100644
--- a/biblio.bib
+++ b/biblio.bib
@@ -19,3 +19,102 @@
   year={1980},
   isbn={0387102353}
 }
+
+%%%%% Pierre's references
+
+@article{hyland2000full,
+  title={On full abstraction for PCF: I, II, and III},
+  author={Hyland, J Martin E and Ong, C-HL},
+  journal={Information and computation},
+  volume={163},
+  number={2},
+  pages={285--408},
+  year={2000},
+  publisher={Elsevier}
+}
+
+@article{abramsky2000full,
+  title={Full abstraction for PCF},
+  author={Abramsky, Samson and Jagadeesan, Radha and Malacaria, Pasquale},
+  journal={Information and Computation},
+  volume={163},
+  number={2},
+  pages={409--470},
+  year={2000},
+  publisher={Elsevier}
+}
+
+@article{abramsky1996linearity,
+  title={Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions},
+  author={Abramsky, Samson and McCusker, Guy},
+  journal={Electronic Notes in Theoretical Computer Science},
+  volume={3},
+  pages={2--14},
+  year={1996},
+  publisher={Elsevier}
+}
+
+@inproceedings{laird1997full,
+  title={Full abstraction for functional languages with control},
+  author={Laird, James},
+  booktitle={Logic in Computer Science, 1997. LICS'97. Proceedings., 12th Annual IEEE Symposium on},
+  pages={58--67},
+  year={1997},
+  organization={IEEE}
+}
+
+@inproceedings{abramsky1998fully,
+  title={A fully abstract game semantics for general references},
+  author={Abramsky, Samson and Honda, Kohei and McCusker, Guy},
+  booktitle={Logic in Computer Science, 1998. Proceedings. Thirteenth Annual IEEE Symposium on},
+  pages={334--344},
+  year={1998},
+  organization={IEEE}
+}
+
+@article{laird2001game,
+  title={A game semantics of Idealized CSP},
+  author={Laird, James},
+  journal={Electronic Notes in Theoretical Computer Science},
+  volume={45},
+  pages={232--257},
+  year={2001},
+  publisher={Elsevier}
+}
+
+@inproceedings{ghica2004angelic,
+  title={Angelic semantics of fine-grained concurrency},
+  author={Ghica, Dan R and Murawski, Andrzej S},
+  booktitle={International Conference on Foundations of Software Science and Computation Structures},
+  pages={211--225},
+  year={2004},
+  organization={Springer}
+}
+
+@inproceedings{reynolds1978syntactic,
+  title={Syntactic control of interference},
+  author={Reynolds, John C},
+  booktitle={Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages},
+  pages={39--46},
+  year={1978},
+  organization={ACM}
+}
+
+@inproceedings{caires2010session,
+  title={Session types as intuitionistic linear propositions},
+  author={Caires, Lu{\'\i}s and Pfenning, Frank},
+  booktitle={International Conference on Concurrency Theory},
+  pages={222--236},
+  year={2010},
+  organization={Springer}
+}
+
+@inproceedings{rideau2011concurrent,
+  title={Concurrent Strategies.},
+  author={Rideau, Silvain and Winskel, Glynn},
+  booktitle={LICS},
+  volume={11},
+  pages={409--418},
+  year={2011}
+}
+
diff --git a/concurgames.sty b/concurgames.sty
index c3f5d8f..0ae1207 100644
--- a/concurgames.sty
+++ b/concurgames.sty
@@ -34,6 +34,7 @@
 
 % LCCS
 
+\newcommand{\lccs}{$\lambda$CCS}
 \newcommand{\proc}{\mathbb{P}}
 \newcommand{\chan}{\mathbb{C}}
 
diff --git a/report.tex b/report.tex
index 8c3e17d..5d69aff 100644
--- a/report.tex
+++ b/report.tex
@@ -34,6 +34,14 @@
 
 \tableofcontents
 
+\section{Introduction}
+
+In game semantics, the semantics of programs are represented as a two-players
+game, in which Player plays for the program and Opponent plays for the
+environment of the program (the user, the operating system, \ldots). The
+execution of a program, in this formalism, is then represented as a succession
+of moves.
+
 \section{Existing work}
 
 My work is set in the context of a wider theory, the basics of which are
@@ -118,7 +126,7 @@ events consistent with one another and its Hasse diagram would look like
 	An \emph{event structure}~\cite{winskel1986event} is a pair
 	$(E, \leq_E, \con_E)$, where $E$ is a
 	set of \emph{events}, $\leq_E$ is a partial order on $E$ and
-	$\con_E \subseteq \powerset(E)$ is a set of \emph{consistent events}.
+	$\con_E \subseteq \powerset_F(E)$ is a set of \emph{consistent events}.
 
 	The partial order $\leq_E$ naturally induces a binary relation $\edgeArrow$
 	over $E$ that is defined as the transitive reduction of $\leq_E$.
@@ -148,8 +156,8 @@ reduction of $\leq_E$; onto which the conflict relation is superimposed.
 	function associating a \emph{polarity} to each event.
 \end{definition}
 
-In games theory, this is used to represent whether a move is to be played by
-Player or Opponent.
+In order to model games, this is used to represent whether a move is to be
+played by Player or Opponent.
 
 \begin{definition}[configuration]
 	A \emph{configuration} of an ESP $A$ is a subset $X \subseteq A$
@@ -185,7 +193,7 @@ drink.
 	In this example (and all the following), a red-circled node has a negative
 	polarity, while a green-circled one has a positive polarity.
 
-	Here, the game has only event, but no edges: nothing in the rules of the
+	Here, the game has only events, but no edges: nothing in the rules of the
 	game constrains the program to behave in a certain way, only its
 	\emph{strategy} will do that.
 
@@ -309,10 +317,10 @@ and not just a set where the events from, \eg, $A$ and $B$ are mixed. \\
 This information is kept in a tree, whose leaves are the base games that were
 put in parallel, and whose nodes represent a parallel composition operation.
 
-Finally, a \emph{strategy} is consists in a game and an ESP (the strategy
-itself), plus a map from the nodes of the strategy to the nodes of the game.
-This structure is really close to the mathematical definition of a strategy,
-and yet is only a lesser loss in efficiency.
+Finally, a \emph{strategy} consists in a game and an ESP (the strategy itself),
+plus a map from the nodes of the strategy to the nodes of the game.  This
+structure is really close to the mathematical definition of a strategy, and yet
+is only a lesser loss in efficiency.
 
 \subsection{Operations}
 
@@ -365,8 +373,8 @@ and then computing the transitive reduction of the DAG\@.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \section{Linear lambda-calculus}
 
-Concurrent games can be used as a model of lambda-calculus.
-To avoid non-determinism in the strategies, and to have a somehow easier
+Concurrent games can be used as a model of lambda-calculus.  To keep the
+strategies finite and to avoid non-determinism, and to have a somehow easier
 approach, one can use concurrent games as a model of \emph{linear}
 lambda-calculus, that is, a variant of the simply-typed lambda-calculus where
 each variable in the environment can and must be used exactly once.
@@ -464,11 +472,12 @@ turns out to be a nightmare: it is better to keep the environment ordered by
 the variables introduction order, thus intertwining $\Gamma$ and $\Delta$.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\section{Linear CCS}
+\section{Linear \lccs}
 
-After working on linear lambda calculus, my work shifted to ``linear CCS'',
-that is, CCS (Calculus of Communicating Systems,~\cite{milner1980ccs})
-integrated into the linear lambda calculus described above.
+After working on linear lambda calculus, my work shifted to ``linear \lccs'',
+that is, a variant of CCS (Calculus of Communicating
+Systems,~\cite{milner1980ccs}) integrated into the linear lambda calculus
+described above.
 
 CCS is used as a basic model of multi-threaded systems: its atoms are
 \emph{processes}. Those processes can be put in parallel or in sequential