diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2025-06-26 18:16:14 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2025-06-26 18:16:14 +0100 |
| commit | c9919add0fe4cc64021aa0fe676527199fccd245 (patch) | |
| tree | b4565be638b9f688d4a15df7d514dcc6d8ce72bd /sec | |
| parent | 02895b46ecbf12728d5545cad2361e6751c495a9 (diff) | |
Fix 925--927.
Diffstat (limited to 'sec')
| -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 |