A Framework for Extended Algebraic Data Types

• Abdennadher, S.: Operational semantics and confluence of constraint propagation rules. In: Smolka, G. (ed.) CP 1997. LNCS, vol. 1330, pp. 252–266. Springer, Heidelberg (1997)

  Chapter  Google Scholar 

• Barras, B., Boutin, S., Cornes, C., Courant, J., Filliâtre, J.-C., Herbelin, H., Huet, G., Manoury, P., Muñoz, C., Murthy, C., Parent, C., Paulin- Mohring, C., Saïbi, A., Werner, B.: The Coq Proof Assistant Reference Manual Version 6.1. INRIA-Rocquencourt-CNRS-ENS Lyon (December 1996)

  Google Scholar 

• Cheney, J., Hinze, R.: First-class phantom types. Technical Report CUCIS TR2003-1901, Cornell University (2003)

  Google Scholar 

• Chakravarty, M., Keller, G., Peyton Jones, S.: Associated types synonyms. In: Proc. of ICFP 2005, pp. 241–253. ACM Press, New York (2005)

  Google Scholar 

• Chen, C., Xi, H.: Combining programming with theorem proving. In: Proc. of ICFP 2005, pp. 66–77. ACM Press, New York (2005)

  Google Scholar 

• Duck, G.J., Peyton-Jones, S., Stuckey, P.J., Sulzmann, M.: Sound and decidable type inference for functional dependencies. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 49–63. Springer, Heidelberg (2004)

  Chapter  Google Scholar 

• Frühwirth, T.: Constraint handling rules. In: Montanari, U., Rossi, F. (eds.) CP 1995. LNCS, vol. 976, Springer, Heidelberg (1995)

  Google Scholar 

• Glasgow haskell compiler home page, http://www.haskell.org/ghc/

• Jones, S.J., Jones, M.P., Meijer, E.: Type classes: an exploration of the design space. In: Haskell Workshop (June 1997)

  Google Scholar 

• Jones, M.P.: Qualified Types: Theory and Practice. D. Phil. thesis, Oxford University, Oxford (1992)

  Google Scholar 

• Jones, M.P.: Simplifying and improving qualified types. In: FPCA 1995: Conference on Functional Programming Languages and Computer Architecture. ACM Press, New York (1995)

  Google Scholar 

• Jones, M.P.: Type classes with functional dependencies. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, p. 230. Springer, Heidelberg (2000)

  Chapter  Google Scholar 

• Läufer, K.: Type classes with existential types. Journal of Functional Programming 6(3), 485–517 (1996)

  Article  MathSciNet  MATH  Google Scholar 

• Lassez, J., Maher, M., Marriott, K.: Unification revisited. In: Foundations of Deductive Databases and Logic Programming. Morgan Kauffman, San Francisco (1987)

  Google Scholar 

• Läufer, K., Odersky, M.: Polymorphic type inference and abstract data types. ACM Trans. Program. Lang. Syst. 16(5), 1411–1430 (1994)

  Article  Google Scholar 

• Garrett Morris, J.: GADT question (2005), http://www.haskell.org/pipermail/glasgow-haskell-users/2005-October/009076.html

• Nilsson, H.: Dynamic optimization for functional reactive programming using generalized algebraic data types. In: Proc. of ICFP 2005, pp. 54–65. ACM Press, New York (2005)

  Google Scholar 

• Odersky, M., Sulzmann, M., Wehr, M.: Type inference with constrained types. Theory and Practice of Object Systems 5(1), 35–55 (1999)

  Article  Google Scholar 

• Jones, S.P., Vytiniotis, D., Washburn, G., Weirich, S.: Simple unification-based type inference for GADTs (2005), Submitted to PLDI 2006

  Google Scholar 

• Jones, S.P. (ed.): Haskell 1998 Language and Libraries: The Revised Report. Cambridge University Press, Cambridge (2003)

  Google Scholar 

• Pottier, F., Gauthier, N.: Polymorphic typed defunctionalization. In: Proc. of POPL 2004, pp. 89–98. ACM Press, New York (2004)

  Google Scholar 

• Pottier, F., Régis-Gianas, Y.: Stratified type inference for generalized algebraic data types. In: Proc. of POPL 2006, pp. 232–244. ACM Press, New York (2006)

  Google Scholar 

• Pfenning, F., Schürmann, C.: System description: Twelf - a metalogical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)

  Chapter  Google Scholar 

• Sheard, T.: Putting curry-howard to work. In: Proc. of Haskell 2005, pp. 74–85. ACM Press, New York (2005)

  Google Scholar 

• Shoenfield, J.R.: Mathematical Logic. Addison-Wesley, Reading (1967)

  MATH  Google Scholar 

• Sheard, T., Pasalic, E.: Meta-programming with built-in type equality. In: Fourth International Workshop on Logical Frameworks and Meta-Languages (2004)

  Google Scholar 

• Simonet, V., Pottier, F.: Constraint-based type inference for guarded algebraic data types. Research Report 5462, INRIA (January 2005)

  Google Scholar 

• Stuckey, P.J., Sulzmann, M.: A theory of overloading. ACM Transactions on Programming Languages and Systems (2005) (to appear)

  Google Scholar 

• Sulzmann, M.: A General Framework for Hindley/Milner Type Systems with Constraints. PhD thesis, Yale University, Department of Computer Science (May 2000)

  Google Scholar 

• Sulzmann, M., Wazny, J.: Chameleon, http://www.comp.nus.edu.sg/~sulzmann/chameleon

• Sulzmann, M., Wazny, J.: Lexically scoped type annotations (2005), http://www.comp.nus.edu.sg/~sulzmann

• Sulzmann, M., Wazny, J., Stuckey, P.J.: Co-induction and type improvement in type class proofs (2005), http://www.comp.nus.edu.sg/~sulzmann

• Sulzmann, M., Wazny, J., Stuckey, P.J.: A framework for extended algebraic data types. Technical report, The National University of Singapore (2006)

  Google Scholar 

• Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad-hoc. In: Proc. of POPL 1989, pp. 60–76. ACM Press, New York (1989)

  Google Scholar 

• Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. In: Proc. of POPL 2003, pp. 224–235. ACM Press, New York (2003)

  Google Scholar 

• Zenger, C.: Indizierte Typen. PhD thesis, Universität Karlsruhe (1999)

  Google Scholar 

Download references