%!TEX root = ../Main.tex
\section{Related Work}
We started this work because we could not find a complete formalization of System-F2 with algebraic data that did not use take simplifying shortcuts. At the time of writing, most type theory papers either do not come with mechanized proofs, or present only a ``kernel'' langauge, instead of a full language that could be directly implemented. For example, a count by the author of the recent conference Principles of Programming Languages, POPL 2013 revealed ... type theory papers based on some version of System-F..., of which ... had mechanized proofs and none had mechanized a full language with algebraic data. We hope that this work can serve as a reference implementation to make it easier to present full languages in the future.
AURA proof. \TODO{Check out uses of fully-applied-args in AURA proof.} Allow term language to contain partially applied args but then needs to prove lots of lemmas for it.
\begin{itemize}
\item POPLMark Challenge \cite{Aydemir:POPLmark} explicitly not a ``full language''. Not easy to extract proof engineering principles from these works. Many lemmas crammed into one big file without an obvious module structure, very little comments or auxilliary documentation. No doubt the authors are used to reading the lemma statements, but not easy for newbies.
\item A representation of F$_\omega$ in LF \cite{Schurmann:Fomega-in-LF}. Pure Calculus, no data.
\item Klein machine checked proof for Java like language \cite{Klein:java-like}.
\item Mechanizing metatheory of ML. Only inl inr, not full cases. ``Equivalent Expressive Power''\cite{Lee:mechanized-ML}.
\item Familty of lambda calculi with references \cite{Papakyriakou:mechanized-lambda-ref}. Has System F, but no data.
\end{itemize}