diff --git a/concurgames.sty b/concurgames.sty
index 027cc7d..f75071e 100644
--- a/concurgames.sty
+++ b/concurgames.sty
@@ -5,6 +5,7 @@
 \usepackage{MnSymbol}
 \usepackage{stmaryrd}
 \usepackage{tikz}
+\usepackage{relsize}
 
 \usetikzlibrary{shapes,arrows}
 
@@ -28,6 +29,9 @@
 
 \newcommand{\seman}[1]{\llbracket{} #1 \rrbracket}
 
+\newcommand{\tens}{\otimes}
+\newcommand{\Tens}{\mathlarger\otimes}
+
 \newcommand{\includedot}[2][]{%
 	\begin{tikzpicture}[>=latex,line join=bevel,#1]
 	\input{_build/dot/#2.tex}
diff --git a/report.tex b/report.tex
index d8bbfa4..a139e30 100644
--- a/report.tex
+++ b/report.tex
@@ -301,12 +301,32 @@ and then computing the transitive reduction of the DAG\@.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \section{Linear lambda-calculus}
 
-Concurrent games can be used as a model of lambda-calculus \todo{ref Pierre~?}.
+Concurrent games can be used as a model of lambda-calculus.
 To avoid non-determinism in the strategies, 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.
 
+\subsection{Definition}
+
+The linear lambda calculus we use has the same syntax as the usual simply-typed
+lambda calculus with type annotations and tensor product:
+
+\begin{minipage}[t]{0.45\textwidth}
+	\begin{align*}
+		\text{Terms } t,u,\ldots ::=~&x \in \mathbb{V} \\
+		\vert~&t~u \\
+		\vert~&\lambda x^A \cdot t \\
+		\vert~&t \tens u
+	\end{align*}
+\end{minipage} \hfill \begin{minipage}[t]{0.45\textwidth}
+	\begin{align*}
+		\text{Types } A,B,\ldots ::=~&\alpha \\
+		\vert~&A \linArrow B \\
+		\vert~&A \Tens B
+	\end{align*}
+\end{minipage}
+
 \begin{minipage}{0.4\textwidth} \begin{equation}
 	\tag{\textit{Ax}}
 	\frac{}{x : A \vdash x : A}
@@ -322,7 +342,6 @@ each variable in the environment can and must be used exactly once.
 	\label{typ:llam:app}
 \end{align} \end{minipage}
 
-\todo{describe linear lambda-calculus?}
 
 The implementation, which was supposed to be fairly simple, turned out to be
 not as trivial as expected due to technical details: while, in the theory, the