formalism: Give brief description of typed action calculus

hazelgrove · Oct 8, 2023 · 33ed96a · 33ed96a
1 parent 226af80
commit 33ed96a
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/formalism/typed.tex b/formalism/typed.tex
@@ -9,6 +9,10 @@
 
 \section{Typed hazelnut}
 \label{sec:typed}
+We now give a description of a \emph{typed} version of the Hazelnut action calculus that
+incorporates the marked lambda calculus to solve the problem of non-local hole fixes. Here, unlike
+in the integration of the untyped version and the marked lambda calculus given in
+\cref{sec:untyped}, remarking is performed only when necessary instead of after every action.
 
 \subsection{Syntax}
 \label{sec:typed-syntax}