diff options
Diffstat (limited to 'sec/reducer.ltx')
| -rw-r--r-- | sec/reducer.ltx | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/sec/reducer.ltx b/sec/reducer.ltx index a781a0c..2eaca08 100644 --- a/sec/reducer.ltx +++ b/sec/reducer.ltx @@ -129,6 +129,14 @@ let step (t : Term) : Term = \subsection{Encoding Algorithm}% \label{subsec:encoding} +In \cref{M-sec:encoding} we described a process to embed \lang{} +within System~T. We have written this algorithm in \lang{} itself, +simultaneously mechanising the conversion and proving it is +terminating. Our input is type-annotated \lang{} terms, and we output +unannotated System~T terms as in \cref{lst:term-ty}. Each phase is +accompanied by its own inductive types representing types and +type-annotated terms. + \TODO{ \begin{itemize} \item describe the inputs to the embedding |