%!TEX root = ../Main.tex
\section{Introduction}
Simplifying a language semantics to make the soundness proof easier creates a mismatch between what is proved and what will actually be implemented. A common simplification is to flatten out case-matching expressions, so that what was a \emph{list} of alternatives in the original semantics becomes a sequence of matches of two alternatives each. Another simplification is to reduce the set of evaluation contexts, so that the formalization requires the program to be in administrative normal (a-normal) form. However, when such a language is used as the intermediate representation (IR) for a compiler, it typically performs transformations on nested terms, only converting to a-normal form occasionally.
The standard justification is that a program in the bigger language could always be converted to the simpler version and type-checked there --- but unless the compiler itself is to be formally verified, this conversion is unlikely to be done in practice. The question we seek to answer in this paper is: how bad is it to formalize the real language? We take a standard core language without simplification and prove it sound, not shirking from unsightly proof goals. Having done so, we have found one major difficulty involving evaluation contexts, which we have factored out into a reusable library.
In summary, we make the following contributions \TODO{expand this}.
\begin{itemize}
\item We provide a soundness proof for System-F2 with algebraic data as it would be used as a compiler IR, without simplifications to sweeten the job.
\item We introduce \emph{joint evaluation contexts} which abstract over the problem of identifying the next expression to reduce in a list that may or may not contain redexes.
\end{itemize}