\documentclass{svjour3}

\date{Received: date / Accepted: date}



%include lhs2TeX.fmt
%include polycode.fmt

\usepackage{amsmath}
\usepackage{graphicx}
\usepackage{amssymb}
\usepackage{fancyvrb}
\usepackage[english]{babel}
\usepackage{xcolor}
\usepackage{mainsty}
\usepackage{mathpartir}
\usepackage{stmaryrd}
\usepackage{natbib}


\title{A Lean Specification for GADTs: System F with First-class Equality Proofs}
\titlerunning{System F with First-class Equality Proofs}
\author{Arie Middelkoop \and Atze Dijkstra \and S. Doaitse Swierstra}
\institute{
  Arie Middelkoop \and Atze Dijkstra \and S. Doaitse Swierstra \at
  Universiteit Utrecht\\
  Department of Information and Computing Sciences\\
  Tel.: +31 30 253 3261\\
  Fax: +31 30 253 2804\\
  \email{\{ariem,atze,doaitse\}@@cs.uu.nl}
}

\smartqed
\begin{document}

\newcommand{\Fig}[1]{Figure~\ref{#1}}
\newcommand{\Sect}[1]{Section~\ref{#1}}
\newcommand{\SystemF}{System $F\,$}
\newcommand{\SystemFA}{System $F_A\,$}
\newcommand{\SystemFAPrime}{System $F_A'\,$}
%%\newcommand{\SystemFAI}{System $F_A^i$}
\newcommand{\SystemFAI}{System $F_{|~|}$}
\newcommand{\SystemFC}{System $F_C$}
\newcommand{\GADT}{GADT }
\newcommand{\GADTs}{GADTs}


%%\newcommand{\metacomment}[1] {\begin{quote}\begin{tiny}\begin{color}{blue}\begin{itemize} #1 \end{itemize}\end{color}\end{tiny}\end{quote}}
\newcommand{\metacomment}[1] {}


%include format.lhs
%% %include rules.lhs


\maketitle

\begin{abstract}
Generalized Algebraic Data Types are a generalization of Algebraic Data Types
with additional type equality constraints. These found their use in many functional
programs, including the development of embedded domain specific programming languages and
generic programming.

Recently, several authors published novel inference algorithms and
corresponding type system specifications.
These approaches tend to be more algorithmic than declarative in
nature, and tied to a given compiler infrastructure. This results in
complex specifications.
For a language implementor,
adopting such a complex approach is hard, due to conflicting infrastructure and
language features. Similarly, type inference is difficult to comprehend
for a programmer when the specification is complex.

To make the integration of GADTs in languages easier, we thus need a more orthogonal
specification. We present an orthogonal specification for GADTs:
the language \SystemFAI, consisting of
System F augmented with first-class equality proofs.
This specification exploits the Church encoding of
data types to describe GADT matches in terms of conventional
lambda abstractions.
\end{abstract}

\keywords{Type System \and GADT \and System F \and Equality Proof}


%include introduction.lhs
%include motivation.lhs
%include typesystem.lhs
%include translation.lhs
%% %include algorithm.lhs
%include related-work.lhs
%include conclusion.lhs

\begin{acknowledgements}
This work was supported by Microsoft Research through its European PhD Scholarship Programme.
We thank the anonymous reviewers of TFP 08 and TFP-HOSC
for extensive comments on earlier versions of this paper.
\end{acknowledgements}


%if False
\appendix
%include appendices.lhs
%endif


\bibliographystyle{spbasic}
\bibliography{gadt-paper}

\end{document}