Slight rewording

thesis.bib

@@ -769,6 +769,28 @@
  address = {Cambridge, MA, USA},
 }
 
+# OCaml
+@book{LeroyDFGRV20,
+ author = {Xavier Leroy and Damien Doligez and Alain Frisch and Jacques Garrigue and Didier Rémy and Jérôme Vouillon},
+ title = {The {OCaml} System Release 4.11: Documentation and user's manual},
+ year = 2020,
+ month = aug,
+ publisher = {Institut National de Recherche en Informatique et en Automatique}
+}
+
+# Scheme R6RS
+@book{SperberDFSFM10,
+  author    = {Michael Sperber and
+               R. Kent Dybvig and
+               Matthew Flatt and
+               Anton van Straaten and
+               Robert Bruce Findler and
+               Jacob Matthews},
+  title     = {Revised6 Report on the Algorithmic Language Scheme},
+  publisher = {Cambridge University Press},
+  year      = {2010}
+}
+
 # Timeless classics
 @article{Plotkin04a,
   author    = {Gordon D. Plotkin},
@@ -813,7 +835,7 @@
   year      = {1994}
 }
 
-% Control operators
+# Control operators
 @article{Landin65,
   author    = {Peter J. Landin},
   title     = {Correspondence between {ALGOL} 60 and Church's Lambda-notation: part
@@ -846,7 +868,7 @@
   year      = {1998}
 }
 
-% System F
+# System F
 @phdthesis{Girard72,
   author = {J. Y. Girard},
   school = {Universit{\'e} Paris 7},
@@ -875,3 +897,12 @@
   year      = {1989}
 }
 
+# Tail calls
+@inproceedings{Clinger98,
+  author    = {William D. Clinger},
+  title     = {Proper Tail Recursion and Space Efficiency},
+  booktitle = {{PLDI}},
+  pages     = {174--185},
+  publisher = {{ACM}},
+  year      = {1998}
+}

thesis.tex

@@ -881,6 +881,63 @@ bindings, pair deconstructing, and case splitting. In each of those
 cases we subtract the relevant binder(s) from the set of free
 variables.
 
+\paragraph{Proper tail-recursion}
+
+Many implementations of functional programming languages to be
+tail-recursive in order to enable unbounded iteration as otherwise
+nested repeated function calls would quickly run out of space on a
+computer.
+%
+Intuitively, tail-recursion permits an already allocated stack frame
+for some on-going function call to be reused by a nested function
+call, provided that this nested call is the last thing to occur before
+returning from the on-going function call.
+%
+Any decent implementation of Standard ML~\cite{MilnerTHM97},
+OCaml~\cite{LeroyDFGRV20}, or Scheme~\cite{SperberDFSFM10} will be
+tail-recursive. I intentionally say implementation, because it is
+often the case that the specification or user manual does not
+explicitly require a suitable implementation to be tail-recursive; in
+fact of the three languages just mentioned only Scheme mandates an
+implementation to be tail-recursive.
+%
+The Scheme specification actually goes further and demands that an
+implementation is \emph{properly tail-recursive}, which provides
+strict guarantees on the asymptotic space consumption of tail
+calls~\cite{Clinger98}.
+
+Tail calls will become important in Chapter~\ref{ch:cps} where we will
+get to discuss continuation passing style as an implementation
+technique for effect handlers, as tail calls are ubiquitous in
+continuation passing style.
+%
+Therefore let us formally characterise tail calls by adapting a
+syntactic characterisation due to \citet{Clinger98}.
+%
+\begin{definition}[Tail computation]\label{def:tail-comp}
+  The notion of tail computation is defined inductively as follows.
+  %
+  \begin{itemize}
+    \item The body $M$ of a $\lambda$-abstraction ($\lambda x. M$) is a
+      tail computation.
+    \item If $\Case\;V\;\{\ell\,x \mapsto M; y \mapsto N\}$ is a tail
+      computation, then both $M$ and $N$ are tail computations.
+    \item If $\Let\;\Record{\ell = x; y} = V \;\In\;N$ is a tail
+      computation, then $N$ is a tail computation.
+    \item If $\Let\;x \revto M\;\In\;N$ is a tail computation, then
+      $N$ is a tail computation.
+    \item Nothing else is a tail computation.
+  \end{itemize}
+\end{definition}
+%
+\begin{definition}[Tail call]\label{def:tail-call}
+  A tail call is tail computation that has the form $V\,W$.
+\end{definition}
+%
+The syntactic position of a tail call is often referred to as the
+\emph{tail-position}.
+%
+
 \subsection{Typing rules}
 \label{sec:base-language-type-rules}
 %