diff options
| -rw-r--r-- | sec/compiler.ltx | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/sec/compiler.ltx b/sec/compiler.ltx index 3a3cebc..efe7cf2 100644 --- a/sec/compiler.ltx +++ b/sec/compiler.ltx @@ -17,7 +17,8 @@ three main components: \item Second we perform type checking using a bidirectional algorithm~\cite{bidir}. Along with the usual type checking result, - the algorithm produces a runtime-erased typing derivation. + the algorithm produces a runtime-erased certificate that a term is + well/ill typed. \item Finally we compile the term to Guile~Scheme~\cite{guile}. By requiring an erased type derivation, the compiler can statically |