diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2025-06-24 17:58:53 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2025-06-24 17:58:53 +0100 |
| commit | e6533c9152bb489b4804f5cdbe0c4d57893d3854 (patch) | |
| tree | 5ef217cfa287c93b03f2a3aac8dd3a522a3f7979 | |
| parent | 66450ee5c829e7c00ffa3fca786b4e65bc7c5733 (diff) | |
Fix 38--41.
| -rw-r--r-- | sec/intro.ltx | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/sec/intro.ltx b/sec/intro.ltx index e60410a..26b3a7d 100644 --- a/sec/intro.ltx +++ b/sec/intro.ltx @@ -52,7 +52,9 @@ Developing these non-trivial recursive programs requires good tools for using \lang{}. To that end, we have implemented a certifying type checker and a compiler into Scheme. Our type checker not only checks whether a \lang{} program is well/ill-typed, but it also provides a -proof for its decision. +proof for its decision. The compiler needs this certificate when +compiling \lang{} into Scheme, so that it has enough type information +to compile \foldkw{}. \subsubsection*{Contributions}% In this paper we: |