diff --git a/concurgames.sty b/concurgames.sty
index 250690b..a87b473 100644
--- a/concurgames.sty
+++ b/concurgames.sty
@@ -36,6 +36,7 @@
 
 % LCCS
 
+\newcommand{\lcalc}{$\lambda$-calculus}
 \newcommand{\lccs}{$\lambda$CCS}
 \newcommand{\llccs}{$\lambda$CCS$_\linarrow$}
 \newcommand{\proc}{\mathbb{P}}
diff --git a/report.tex b/report.tex
index eb7e076..c43bb38 100644
--- a/report.tex
+++ b/report.tex
@@ -36,7 +36,7 @@
 
 \section{Introduction}
 
-\paragraph{Game semantics} are a kind of operational semantics in which a
+\paragraph{Game semantics} are a kind of denotational semantics in which a
 program's behavior 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
@@ -70,12 +70,12 @@ 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
-\fname{Laird}~\cite{laird2001game}, introducing game semantics for a
-$\lambda$-calculus 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} laid the first stone
-by defining game semantics for a fine-grained concurrent language including
-parallel execution of ``threads'' and low-level semaphores.
+\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} laid the first stone by defining
+game semantics for a fine-grained concurrent language including parallel
+execution of ``threads'' and low-level semaphores.
 
 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
@@ -114,6 +114,12 @@ could not be reached --- but is not so far away ---, we have proved the
 obtained an implementation of the (denotational) game semantics, that is, code
 that translates a term of the language into its corresponding strategy.
 
+\section{A linear \lcalc{} with concurrency primitives: \llccs}
+
+\subsection{A linear variant of CCS}
+
+\subsection{Lifting to the higher order: linear \lcalc}
+
 \section{Existing work}
 
 My work is set in the context of a wider theory, the basics of which are