Add introduction skeleton and contributions.

1 files changed, 34 insertions, 1 deletions

diff --git a/sec/intro.ltx b/sec/intro.ltx
index 0cd7b1d..0a50ff4 100644
--- a/sec/intro.ltx
+++ b/sec/intro.ltx
@@ -4,6 +4,39 @@
 \section{Introduction}%
 \label{sec:intro}
 
-\TODO{}
+\TODO{
+\begin{itemize}
+  \item System~T is a STLC with natural numbers and primitive
+    recursors
+  \item Arguably simplest system for higher order computation
+  \item Explore expressive power by creating lang. encodes into Sys~T
+  \item \lang{} adds regular types to Sys~T
+  \item Example: compose binary tree of functions
+  \item Explain weird fold syntax
+  \item All \lang{} programs strongly normalise
+  \item Can do most programming
+  \item Write encoding alg. in \lang{}
+  \item Write fuelled Sys~T reducer
+  \item Developing non-trivial progs needs good tools
+  \item Have a certifying type checker and a compiler
+\end{itemize}
+}
+
+\subsubsection*{Contributions}%
+In this paper we:
+\begin{itemize}
+  \item contrast different methods for encoding inductive types in
+    System~T (\cref{M-subsec:encoding-strategies});
+  \item give the syntax, typing rules and equational theory for
+    \lang{} (\cref{M-sec:lang});
+  \item explain how to encode \lang{} into System~T by giving a
+    seven-phase encoding algorithm (\cref{M-sec:encoding});
+  \item demonstrate usability of \lang{} over System~T by writing a
+    fuelled System~T reducer (\cref{M-subsec:reducer});
+  \item demonstrate expressiveness of \lang{} by writing the encoding
+    algorithm within \lang{} (\cref{M-subsec:encoding}); and
+  \item describe a certifying type checker and a compiler for \lang{}
+    implemented in Idris~2 (\cref{M-sec:compiler}).
+\end{itemize}
 
 \end{document}