References

  1. Lennart Augustsson & Kent Petersson (1994): Silly Type Families. Draft.
  2. James Cheney & Ralf Hinze (2003): First-Class Phantom Types. Technical Report CUCIS TR2003-1901. Cornell University.
  3. Thierry Coquand (1992): Pattern Matching with Dependent Types. In: Proc. Workshop on Types for Proofs and Programs, pp. 71–83.
  4. Joshua Dunfield (2007): A Unified System of Type Refinements. Carnegie Mellon University. CMU-CS-07-129.
  5. Jacques Garrigue (1998): Programming with Polymorphic Variants. In: ML Workshop, Baltimore.
  6. Jacques Garrigue & Jacques Le Normand (2011): Adding GADTs to OCaml: the direct approach. In: Workshop on ML, Tokyo.
  7. 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.
  8. 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.
  9. Fabrice Le Fessant & Luc Maranget (2001): Optimizing Pattern Matching. In: Proc. International Conference on Functional Programming, pp. 26–37, doi:10.1145/507635.507641.
  10. 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.
  11. Luc Maranget (2007): Warnings for pattern matching. Journal of Functional Programming 17(3), pp. 387–421, doi:10.1017/S0956796807006223.
  12. Conor McBride (1999): Dependently Typed Functional Programs and their Proofs. Doctor of philosophy. University of Edinburgh.
  13. Ulf Norell (2007): Towards a practical programming language based on dependent type theory. Chalmers University of Technology and Göteborg University.
  14. 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.
  15. 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.
  16. 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.
  17. 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.
  18. OCaml bug tracker (2014): GADT exhaustiveness check incompleteness. OCaml problem report #6437. http://caml.inria.fr/mantis/view.php?id=6437.
  19. 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.
  20. 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.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org