\documentclass[../main.tex]{subfiles}

\begin{document}
\section{Introduction}%
\label{sec:intro}

\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}[nosep]
  \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}