Thierry Coquand (1992):
Pattern Matching with Dependent Types.
In: Proc. Workshop on Types for Proofs and Programs,
pp. 71–83.
Joshua Dunfield (2007):
A Unified System of Type Refinements.
Carnegie Mellon University.
CMU-CS-07-129.
Jacques Garrigue (1998):
Programming with Polymorphic Variants.
In: ML Workshop,
Baltimore.
Jacques Garrigue & Jacques Le Normand (2011):
Adding GADTs to OCaml: the direct approach.
In: Workshop on ML,
Tokyo.
Georgios Karachalias, Tom Schrijvers, Dimitrios Vytiniotis & Simon Peyton Jones (2015):
GADTs meet their match.
In: Proc. International Conference on Functional Programming,
pp. 424–436,
doi:10.1145/2784731.2784748.
Neelakantan R. Krishnaswami (2009):
Focusing on pattern matching.
In: Proc. ACM Symposium on Principles of Programming Languages,
pp. 366–378,
doi:10.1145/1480881.1480927.
Fabrice Le Fessant & Luc Maranget (2001):
Optimizing Pattern Matching.
In: Proc. International Conference on Functional Programming,
pp. 26–37,
doi:10.1145/507635.507641.
Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier Rémy & Jérôme Vouillon (2012):
The OCaml system release 4.00, Documentation and user's manual.
Projet Gallium, INRIA.
Luc Maranget (2007):
Warnings for pattern matching.
Journal of Functional Programming 17(3),
pp. 387–421,
doi:10.1017/S0956796807006223.
Conor McBride (1999):
Dependently Typed Functional Programs and their Proofs.
Doctor of philosophy.
University of Edinburgh.
Ulf Norell (2007):
Towards a practical programming language based on dependent type theory.
Chalmers University of Technology and Göteborg University.
Ulf Norell (2009):
Dependently Typed Programming in Agda.
In: Advanced Functional Programming 2008,
Springer LNCS 5832,
pp. 230–266,
doi:10.1007/978-3-642-04652-0_5.
Nicolas Oury (2007):
Pattern Matching Coverage Checking with Dependent Types Using Set Approximations.
In: Proc. Workshop on Programming Languages Meets Program Verification,
pp. 47–56,
doi:10.1145/1292597.1292606.
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich & Geoffrey Washburn (2006):
Simple unification-based type inference for GADTs.
In: Proc. International Conference on Functional Programming,
pp. 50–61,
doi:10.1145/1159803.1159811.
Carsten Schürmann & Frank Pfenning (2003):
A Coverage Checking Algorithm for LF.
In: Proc. Theorem Proving in Higher Order Logics,
Springer LNCS 2758,
pp. 120–135,
doi:10.1007/10930755_8.
Hongwei Xi (1999):
Dead Code Elimination through Dependent Types.
In: Proc. First International Workshop on Practical Aspects of Declarative Languages,
pp. 228–242,
doi:10.1007/3-540-49201-1_16.
Hongwei Xi, Chiyan Chen & Gang Chen (2003):
Guarded Recursive Datatype Constructors.
In: Proc. ACM Symposium on Principles of Programming Languages.
ACM Press,
pp. 224–235,
doi:10.1145/604131.604150.