1. A. Abel, R. Matthes & T. Uustalu (2005): Iteration and coiteration schemes for higher-order and nested datatypes.. Theor. Comput. Sci. 333(1-2), pp. 3–66, doi:10.1016/j.tcs.2004.10.017.
  2. H. Barendregt (1992): Lambda Calculi with Types. In: Hand. of Logic in Co. Sc.. Oxford, pp. 117–309.
  3. Y. Bertot & P. Casteran (2004): Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Springer, doi:10.1007/978-3-662-07964-5.
  4. M. Churchill, P. D. Mosses, N. Sculthorpe & P. Torrini (2015): Reusable Components of Semantic Specifications. In: TAOSD 12, LNCS 8989. Springer, pp. 132–179, doi:10.1007/978-3-662-46734-3_4.
  5. T. Coquand & G. Huet (1988): The calculus of constructions. Information and Computation 76, pp. 95–120, doi:10.1016/0890-5401(88)90005-3.
  6. B. Delaware, S. Keuchel, T. Schrijvers & B. C.d.S. Oliveira (2013): Modular Monadic Meta-theory. In: ICFP'13. ACM, pp. 319–330, doi:10.1145/2500365.2500587.
  7. B. Delaware, B. C. d. S. Oliveira & T. Schrijvers (2013): Meta-theory à la carte. In: Proc. POPL '13, pp. 207–218, doi:10.1145/2429069.2429094.
  8. N. Ghani, T. Uustalu & V. Vene (2004): Build, Augment and Destroy, Universally. In: Proc. APLAS '04, pp. 327–347, doi:10.1007/978-3-540-30477-7_22.
  9. T. Hagino (1987): A Typed Lambda Calculus with Categorical Type Constructors. In: Category Theory and Computer Science, pp. 140–157, doi:10.1007/3-540-18508-9_24.
  10. G. Hutton (1999): A Tutorial on the Universality and Expressiveness of Fold. J. Funct. Program. 9(4), pp. 355–372, doi:10.1017/S0956796899003500.
  11. S. Keuchel & T. Schrijvers (2013): Generic Datatypes à la Carte. In: 9th ACM SIGPLAN Workshop on Generic Programming (WGP), pp. 1–11, doi:10.1145/2502488.2502491.
  12. N. P. Mendler (1991): Inductive Types and Type Constraints in the Second-Order lambda Calculus. Ann. Pure Appl. Logic 51(1-2), pp. 159–172, doi:10.1016/0168-0072(91)90069-X.
  13. F. Pfenning & C. Paulin-Mohring (1989): Inductively Defined Types in the Calculus of Constructions. In: Math. Foundations of Programming Semantics, pp. 209–228, doi:10.1007/BFb0040259.
  14. G. D. Plotkin (2004): A structural approach to operational semantics. J. Log. Algebr. Program. 60-61, pp. 17–139, doi:10.1016/j.jlap.2004.03.009.
  15. P. Sewell, F. Zappa Nardelli, S. Owens, G. Peskine, T. Ridge, S. Sarkar & R. Strniša (2010): Ott: Effective Tool Support for the Working Semanticist. Journal of Functional Programming 20(1), pp. 71–122, doi:10.1017/S0956796809990293.
  16. W. Swierstra (2008): Data types à la carte. Journal of Functional Programming 18(4), pp. 423–436, doi:10.1017/S0956796808006758.
  17. P. Torrini (2015): Language specification and type preservation proofs in Coq – companion code. Available at
  18. T. Uustalu & V. Vene (1999): Mendler-Style Inductive Types, Categorically. Nord. J. Comput. 6(3), pp. 343.
  19. P. Wadler (1990): Recursive types for free!. Available at

Comments and questions to:
For website issues: