diff --git a/thesis.bib b/thesis.bib index 6b6b8d9..117c509 100644 --- a/thesis.bib +++ b/thesis.bib @@ -1258,7 +1258,7 @@ @techreport{Remy93, title = {{Syntactic theories and the algebra of record terms}}, - author = {Didier Remy}, + author = {Didier R\'{e}my}, number = {RR-1869}, institution = {{INRIA}}, year = {1993}, diff --git a/thesis.tex b/thesis.tex index 9c8b676..3ec498e 100644 --- a/thesis.tex +++ b/thesis.tex @@ -13570,10 +13570,10 @@ Figure~\ref{fig:bpcf} depicts the type syntax, type environment syntax, and term syntax of $\BPCF$. % The main difference in the type language between $\BCalc$ and $\BPCF$ -is that the latter does feature polymorphism and an effect tracking -system. At the term level, $\BPCF$ does not feature polymorphic -records and variants, but rather plain pairs and sums. For sums the -left injection is introduced by $(\Inl~V)^B$, where the type +is that the latter does not feature polymorphism nor an effect +tracking system. At the term level, $\BPCF$ does not feature +polymorphic records and variants, but rather plain pairs and sums. For +sums the left injection is introduced by $(\Inl~V)^B$, where the type annotation $B$ is the type of the right injection. Similarly, the right injection is introduced by $(\Inl~W)^A$, where $A$ is the type of the left injection. The $\Case$-construct eliminates sums. The last @@ -14258,7 +14258,8 @@ The syntax is extended as follows. % The notion of configurations changes slightly as the continuation component is replaced by a generalised continuation -$\kappa \in \MGContCat$, just as described in Chapter~\ref{ch:abstract-machine}% ; a continuation is now a list of +$\kappa \in \MGContCat$, in the same way as described in +Chapter~\ref{ch:abstract-machine}.% ; a continuation is now a list of % resumptions. A resumption is a pair of a pure continuation (as in the % base machine) and a handler closure ($\chi$). %