@unpublished(AugustssonSilly94,
 author       = {Lennart Augustsson and Kent Petersson},
 year         = {1994},
 title        = {Silly Type Families},
 note         = {Draft},
)
@techreport(Cheney2003,
 author       = {James Cheney and Ralf Hinze},
 year         = {2003},
 title        = {First-Class Phantom Types},
 type         = {Technical Report CUCIS},
 number       = {TR2003-1901},
 institution  = {Cornell University},
)
@inproceedings(Coquand92,
 author       = {Thierry Coquand},
 year         = {1992},
 title        = {Pattern Matching with Dependent Types},
 booktitle    = {Proc. Workshop on Types for Proofs and Programs},
 pages        = {71--83},
)
@phdthesis(Dunfield2007phd,
 author       = {Joshua Dunfield},
 year         = {2007},
 title        = {A Unified System of Type Refinements},
 school       = {Carnegie Mellon University},
 note         = {CMU-CS-07-129},
)
@inproceedings(Garrigue98,
 author       = {Jacques Garrigue},
 year         = {1998},
 title        = {Programming with Polymorphic Variants},
 booktitle    = {ML Workshop},
 address      = {Baltimore},
)
@inproceedings(Garrigue2011,
 author       = {Jacques Garrigue and Jacques Le Normand},
 year         = {2011},
 title        = {Adding {GADTs} to {OCaml}: the direct approach},
 booktitle    = {Workshop on ML},
 address      = {Tokyo},
)
@inproceedings(Karachalias2015,
 author       = {Georgios Karachalias and Tom Schrijvers and Dimitrios Vytiniotis and Simon Peyton Jones},
 year         = {2015},
 title        = {{GADTs} meet their match},
 booktitle    = {Proc. International Conference on Functional Programming},
 pages        = {424--436},
 doi          = {10.1145/2784731.2784748},
)
@inproceedings(Krishnaswami2009popl,
 author       = {Neelakantan R. Krishnaswami},
 year         = {2009},
 title        = {Focusing on pattern matching},
 booktitle    = {Proc. ACM Symposium on Principles of Programming Languages},
 pages        = {366--378},
 doi          = {10.1145/1480881.1480927},
)
@inproceedings(LeFessant2001icfp,
 author       = {Le Fessant, Fabrice and Luc Maranget},
 year         = {2001},
 title        = {Optimizing Pattern Matching},
 booktitle    = {Proc. International Conference on Functional Programming},
 pages        = {26--37},
 doi          = {10.1145/507635.507641},
)
@manual(OCaml400,
 author       = {Xavier Leroy and Damien Doligez and Alain Frisch and Jacques Garrigue and Didier R{\'e}my and J{\'e}r{\^o}me Vouillon},
 year         = {2012},
 title        = {The {OCaml} system release 4.00, Documentation and user's manual},
 organization = {Projet Gallium, INRIA},
)
@article(Maranget2007,
 author       = {Luc Maranget},
 year         = {2007},
 title        = {Warnings for pattern matching},
 journal      = {Journal of Functional Programming},
 volume       = {17},
 number       = {3},
 pages        = {387--421},
 doi          = {10.1017/S0956796807006223},
)
@phdthesis(McBride99phd,
 author       = {Conor McBride},
 year         = {1999},
 title        = {Dependently Typed Functional Programs and their Proofs},
 type         = {Doctor of philosophy},
 school       = {University of Edinburgh},
)
@phdthesis(Norell2007phd,
 author       = {Ulf Norell},
 year         = {2007},
 title        = {Towards a practical programming language based on dependent type theory},
 school       = {Chalmers University of Technology and G{\"o}teborg University},
)
@inproceedings(Norell2008,
 author       = {Ulf Norell},
 year         = {2009},
 title        = {Dependently Typed Programming in {Agda}},
 booktitle    = {Advanced Functional Programming 2008},
 series       = {Springer LNCS},
 volume       = {5832},
 pages        = {230--266},
 doi          = {10.1007/978-3-642-04652-0\_5},
)
@inproceedings(Oury2007pplv,
 author       = {Nicolas Oury},
 year         = {2007},
 title        = {Pattern Matching Coverage Checking with Dependent Types Using Set Approximations},
 booktitle    = {Proc. Workshop on Programming Languages Meets Program Verification},
 pages        = {47--56},
 doi          = {10.1145/1292597.1292606},
)
@inproceedings(Peyton2006,
 author       = {{Peyton Jones}, Simon and Dimitrios Vytiniotis and Stephanie Weirich and Geoffrey Washburn},
 year         = {2006},
 title        = {Simple unification-based type inference for {GADTs}},
 booktitle    = {Proc. International Conference on Functional Programming},
 pages        = {50--61},
 doi          = {10.1145/1159803.1159811},
)
@inproceedings(Schurmann2003,
 author       = {Carsten Sch{\"u}rmann and Frank Pfenning},
 year         = {2003},
 title        = {A Coverage Checking Algorithm for LF},
 booktitle    = {Proc. Theorem Proving in Higher Order Logics},
 series       = {Springer LNCS},
 volume       = {2758},
 pages        = {120--135},
 doi          = {10.1007/10930755\_8},
)
@misc(PR6437,
 author       = {OCaml bug tracker},
 year         = {2014},
 title        = {{GADT} exhaustiveness check incompleteness},
 howpublished = {OCaml problem report \#6437},
 note         = {\hbox{\url{http://caml.inria.fr/mantis/view.php?id=6437}}},
)
@inproceedings(Xi99padl,
 author       = {Hongwei Xi},
 year         = {1999},
 title        = {Dead Code Elimination through Dependent Types},
 booktitle    = {Proc. First International Workshop on Practical Aspects of Declarative Languages},
 pages        = {228--242},
 doi          = {10.1007/3-540-49201-1\_16},
)
@inproceedings(Xi2003popl,
 author       = {Hongwei Xi and Chiyan Chen and Gang Chen},
 year         = {2003},
 title        = {Guarded Recursive Datatype Constructors},
 booktitle    = {Proc. ACM Symposium on Principles of Programming Languages},
 publisher    = {ACM Press},
 pages        = {224--235},
 doi          = {10.1145/604131.604150},
)