diff options
Diffstat (limited to 'sec')
| -rw-r--r-- | sec/intro.ltx | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/sec/intro.ltx b/sec/intro.ltx index 9baaf3f..e60410a 100644 --- a/sec/intro.ltx +++ b/sec/intro.ltx @@ -38,15 +38,15 @@ eliminator style to ensure all recursion is structural. If we used explicit recursion, we would need complex checks for structural recursion, like in Agda~\cite{agda} and Idris~2~\cite{idris}. -As we can encode all \lang{} programs into System~T, \lang{} inherit +As we can encode all \lang{} programs into System~T, \lang{} inherits some of System~T's metatheory for free. In particular, as System~T is strongly normalising~\cite{syst-sn}, all \lang{} programs must -terminate. Requiring programs terminate and are well-founded does not -appear to greatly restrict what programs you can write in \lang{}. As -evidence of this, we have written the encoding algorithm from \lang{} -to System~T within \lang{}. We have also produced a fuelled System~T -reducer; given enough fuel, it strongly normalises any well-typed -System~T term. +terminate. Requiring programs to terminate and use structural +recursion does not appear to greatly restrict what programs you can +write in \lang{}. As evidence, we have written the encoding algorithm +from \lang{} to System~T within \lang{} itself. We have also produced +a fuelled System~T reducer; given enough fuel, it strongly normalises +any well-typed System~T term. Developing these non-trivial recursive programs requires good tools for using \lang{}. To that end, we have implemented a certifying type |