Elab properties

impl-paper/conclusions.tex

@@ -5,6 +5,11 @@ \section{Discussion}
 %Discuss performance (anecdotally, how big is the library and how long to check,
 %and relative to previous version). 
 
+\subsection{Performance}
+
+\todo[inline]{Note on performance of type checking, and compilation via Epic. Also
+worth commenting on FFI.}
+
 \subsection{Related Work}
 
 Dependently typed programming languages have becoming more prominent in recent

impl-paper/delab.tex

@@ -118,12 +118,18 @@ \subsection{From \TT{} to \Idris{}}
 
 \subsection{Elaboration Properties}
 
-\todo[inline]{
-What are the properties of elaboration?
-Need to define unelaboration, and say that elaborating then unelaborating
-an expression yields the original expression.
-(Works for expressions but not declarations)
-}
+Elaboration satisfies two important properties. Informally stated, these are
+i) that if elaboration is successful, the
+resulting program is a well-typed \TT{} program; ii) elaboration preserves the
+meaning of the original \Idris{} program. The first property is true by the
+definition of elaboration --- elaboration fails if it attempts to construct an ill-typed
+term at any point. Furthermore, the development calculus \TTdev{} ensures that 
+partial constructions are well-typed.
+
+The second property, that elaboration preserves meaning, can be stated more formally
+as follows: 
+
+If $\MO{Elab}\:\vd\:\mq\:\vt$ then $\MO{Unelab}\:\vt\:\mq\:\vd$
 
 Properties:
 \begin{itemize}

impl-paper/impldtp.tex

@@ -93,6 +93,7 @@
 %theory, using unification and a tactic engine.
 \end{abstract}
 
+
 %\category{D.3.2}{Programming Languages}{Language
 %  Classifications}[Applicative (functional) Languages]
 %\category{D.3.4}{Programming Languages}{Processors}[Compilers]
@@ -136,6 +137,9 @@ \section*{Acknowledgements}
 
 \appendix
 
+\section{TODOs}
+\listoftodos{}
+
 %\section{Elaboration meta-operations}
 
 %It's possible that it would be useful to have a quick reference of meta-operations