Biblio, intro

biblio.bib

@@ -19,3 +19,111 @@
   year={1980},
   isbn={0387102353}
 }
+
+%%%%% Pierre's references
+
+@article{hyland2000pcf,
+  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{abramsky2000pcf,
+  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{laird1997callcc,
+  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{laird2001exceptions,
+  title={A fully abstract game semantics of local exceptions},
+  author={Laird, James},
+  booktitle={Logic in Computer Science, 2001. Proceedings. 16th Annual IEEE Symposium on},
+  pages={105--114},
+  year={2001},
+  organization={IEEE}
+}
+
+@inproceedings{abramsky1998references,
+  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}
+}
+

concurgames.sty

@@ -34,6 +34,7 @@
 
 % LCCS
 
+\newcommand{\lccs}{$\lambda$CCS}
 \newcommand{\proc}{\mathbb{P}}
 \newcommand{\chan}{\mathbb{C}}
 

report.tex

@@ -34,6 +34,32 @@
 
 \tableofcontents
 
+\section{Introduction}
+
+Game semantics are a kind of operational semantics in which a program's
+behaviour is abstracted 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. For instance, the user pressing a
+key on the keyboard would be a move of Opponent, to which Player could react by
+triggering the corresponding action (\eg{} adding the corresponding letter in a
+text field).
+
+Game semantics emerged mostly with~\cite{hyland2000pcf}
+and~\cite{abramsky2000pcf}, independently establishing a fully-abstract model
+for PCF using game semantics, while ``classic'' semantics had failed to provide
+a fully-abstract, reasonable and satisfying model. But this field mostly gained
+in notoriety with the development of techniques to capture additional
+programming languages constructions, among which references
+handling~\cite{abramsky1996linearity}, followed by higher-order
+references~\cite{abramsky1998references}, allowing to model languages with side
+effects; or exception handling~\cite{laird2001exceptions}. Until then, the
+field has been deeply explored, providing a wide range of such constructions in
+the literature.
+
+A success of game semantics is to provide \emph{compositional} and
+\emph{syntax-free} semantics. \qtodo{why?}
+
 \section{Existing work}
 
 My work is set in the context of a wider theory, the basics of which are
@@ -118,7 +144,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 +174,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 +211,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 +335,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 +391,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 +490,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
@@ -616,7 +643,7 @@ execution, and one can synchronize processes on channels.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \bibliography{biblio}
-\bibliographystyle{alpha}
+\bibliographystyle{ieeetr}
 
 \end{document}