\documentclass{llncs}
\usepackage{graphicx}
\usepackage{xspace}
\usepackage{style/utils}
\usepackage{style/code}

% -----------------------------------------------------------------------------
\begin{document}

\title		{Direct formalization of System-F2 \\
                 with algebraic data in Coq}

\author		{Ben Lippmeier}

\institute	{School of Computer Science and Engineering \\ 
		 University of New South Wales \\
		 \email{benl@cse.unsw.edu.au}}
\maketitle

% -- Abstract -----------------------------------------------------------------
\begin{abstract}
Soundness proofs for functional languages typically simplify the semantics in order to make the proof easier. When the language includes algebraic data, common simplifications are to reduce the set of evaluation contexts, and to flatten the case matching form so that it no longer contains a list of alternatives. The result is a ``kernel'' language, which is easier to prove sound but not suitable for direct implementation in a compiler. We present a full proof of soundness for \mbox{System-F2} with algebraic data without using these artificial encodings, and introduce \emph{joint evaluation contexts} to factor out some of the resulting complexity.


\end{abstract}

\makeatactive
% -----------------------------------------------------------------------------
\input{section/01-Introduction.tex}

\clearpage{}
\input{section/02-Encodings.tex}

\clearpage{}
\input{section/03-Language.tex}

\clearpage{}
\input{section/04-JointEvaluation.tex}

\clearpage{}
\input{section/05-Formalization.tex}

\clearpage{}
\input{section/06-Related.tex}

\clearpage{}
\input{section/07-Conclusion.tex}

\clearpage{}
\bibliography{Main}
\bibliographystyle{plain}

\appendix
\clearpage{}
\input{section/A2-TypesOfExps.tex}


\end{document}


