diff options
| -rw-r--r-- | sec/reducer.ltx | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/sec/reducer.ltx b/sec/reducer.ltx index d48e600..c73a4f6 100644 --- a/sec/reducer.ltx +++ b/sec/reducer.ltx @@ -1,13 +1,18 @@ \documentclass[../main.tex]{subfiles} \begin{document} -\section{Writing ARTiST Programs}% +\section{Writing ARTyST Programs}% \label{sec:reducer} +We have used \lang{} to write two non-trivial programs that can be +embedded in System~T. The first is a fuelled reducer for +System~T. Given \(n\) units of fuel, the reducer will perform \(n\) +steps of complete~development~\cite{cd} on a System~T term. The second +program is the encoding from \lang{} to System~T. This takes a +type-annotated \lang{} program and encodes it as a System~T term. + \TODO{ \begin{itemize} - \item state I have written two non-trivial programs in ARTiST - \item briefly describe the fuelled reducer and encoder \item describe the syntactic sugar I have added \end{itemize} } |