diff options
| -rw-r--r-- | sec/compiler.ltx | 20 |
1 files changed, 14 insertions, 6 deletions
diff --git a/sec/compiler.ltx b/sec/compiler.ltx index b4fde16..0948073 100644 --- a/sec/compiler.ltx +++ b/sec/compiler.ltx @@ -17,28 +17,36 @@ three main components: \item Second we perform type checking using a bidirectional algorithm~\cite{bidir}. Along with the usual type checking result, - the algorithm produces a runtime-erased proof that the term is - well-typed. + the algorithm produces a runtime-erased typing derivation. \item Finally we compile the term to Guile~Scheme~\cite{guile}. By - requiring an erased well-typedness proof, the compiler can - statically guarantee it will only ever have to process well-typed - terms. + requiring an erased type derivation, the compiler can statically + guarantee it will only ever have to process well-typed terms. \end{itemize} - +\subsection{Parser} \TODO{ \begin{itemize} + \item summarise \textcite{bidir} + \item explain dependent state \item explain what intentionally well-scoped syntax is \item justify why I used intentionally well-scoped syntax + \end{itemize} +} + +\subsection{Bidirectional Type Checker} +\TODO{ + \begin{itemize} \item describe how type checking produces a derivation \item explain the derivation is runtime erased + \item justify extrinsic derivation \item justify the derivation having no runtime cost \item describe why knowing there is a derivation is necessary \item explain why these extra features do not guarantee compiler correctness \end{itemize} } +\subsection{Scheme Backend} \TODO{ \begin{itemize} \item justify how dynamic types make Scheme a good compilation target |