Biblio, intro

biblio.bib

@@ -22,7 +22,7 @@
 
 %%%%% Pierre's references
 
-@article{hyland2000full,
+@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},
@@ -33,7 +33,7 @@
   publisher={Elsevier}
 }
 
-@article{abramsky2000full,
+@article{abramsky2000pcf,
   title={Full abstraction for PCF},
   author={Abramsky, Samson and Jagadeesan, Radha and Malacaria, Pasquale},
   journal={Information and Computation},
@@ -54,7 +54,7 @@
   publisher={Elsevier}
 }
 
-@inproceedings{laird1997full,
+@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},
@@ -63,7 +63,16 @@
   organization={IEEE}
 }
 
-@inproceedings{abramsky1998fully,
+@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},

report.tex

@@ -36,11 +36,29 @@
 
 \section{Introduction}
 
-In game semantics, the semantics of programs are represented as a two-players
+Game semantics are a kind of operational semantics in which a program's
-game, in which Player plays for the program and Opponent plays for the
+behaviour is abstracted as a two-players game, in which Player plays for the
-environment of the program (the user, the operating system, \ldots). The
+program and Opponent plays for the environment of the program (the user, the
-execution of a program, in this formalism, is then represented as a succession
+operating system, \ldots). The execution of a program, in this formalism, is
-of moves.
+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}
 
@@ -625,7 +643,7 @@ execution, and one can synchronize processes on channels.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \bibliography{biblio}
-\bibliographystyle{alpha}
+\bibliographystyle{ieeetr}
 
 \end{document}