diff options
Diffstat (limited to 'sec/intro.ltx')
| -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: |