@article(AbelMU05,
 author       = {A. Abel and R. Matthes and T. Uustalu},
 year         = {2005},
 title        = {Iteration and coiteration schemes for higher-order and nested datatypes.},
 journal      = {Theor. Comput. Sci.},
 volume       = {333},
 number       = {1-2},
 pages        = {3--66},
 doi          = {10.1016/j.tcs.2004.10.017},
)
@inproceedings(Bar92,
 author       = {H. Barendregt},
 year         = {1992},
 title        = {Lambda Calculi with Types},
 booktitle    = {Hand. of Logic in Co. Sc.},
 publisher    = {Oxford},
 pages        = {117--309},
)
@book(coqart,
 author       = {Y. Bertot and P. Casteran},
 year         = {2004},
 title        = {Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions},
 publisher    = {Springer},
 doi          = {10.1007/978-3-662-07964-5},
)
@incollection(TAOSD,
 author       = {M. Churchill and P. D. Mosses and N. Sculthorpe and P. Torrini},
 year         = {2015},
 title        = {Reusable Components of Semantic Specifications},
 booktitle    = {TAOSD 12},
 series       = {LNCS 8989},
 publisher    = {Springer},
 pages        = {132--179},
 doi          = {10.1007/978-3-662-46734-3\_4},
)
@article(COQ,
 author       = {T. Coquand and G. Huet},
 year         = {1988},
 title        = {The calculus of constructions},
 journal      = {Information and Computation},
 volume       = {76},
 pages        = {95--120},
 doi          = {10.1016/0890-5401(88)90005-3},
)
@inproceedings(Delaware13M,
 author       = {B. Delaware and S. Keuchel and T. Schrijvers and B. C.d.S. Oliveira},
 year         = {2013},
 title        = {Modular Monadic Meta-theory},
 booktitle    = {ICFP'13},
 publisher    = {ACM},
 pages        = {319--330},
 doi          = {10.1145/2500365.2500587},
)
@inproceedings(Dela13,
 author       = {B. Delaware and B. C. d. S. Oliveira and T. Schrijvers},
 year         = {2013},
 title        = {Meta-theory {\`{a}} la carte},
 booktitle    = {Proc. {POPL} '13},
 pages        = {207--218},
 doi          = {10.1145/2429069.2429094},
)
@inproceedings(GhaniUV04,
 author       = {N. Ghani and T. Uustalu and V. Vene},
 year         = {2004},
 title        = {Build, Augment and Destroy, Universally},
 booktitle    = {Proc. {APLAS} '04},
 pages        = {327--347},
 doi          = {10.1007/978-3-540-30477-7\_22},
)
@inproceedings(Hagino87,
 author       = {T. Hagino},
 year         = {1987},
 title        = {A Typed Lambda Calculus with Categorical Type Constructors},
 booktitle    = {Category Theory and Computer Science},
 pages        = {140--157},
 doi          = {10.1007/3-540-18508-9\_24},
)
@article(Hutton99,
 author       = {G. Hutton},
 year         = {1999},
 title        = {A Tutorial on the Universality and Expressiveness of Fold},
 journal      = {J. Funct. Program.},
 volume       = {9},
 number       = {4},
 pages        = {355--372},
 doi          = {10.1017/S0956796899003500},
)
@inproceedings(Keuchel13,
 author       = {S. Keuchel and T. Schrijvers},
 year         = {2013},
 title        = {Generic Datatypes \`{a} la Carte},
 booktitle    = {9th ACM SIGPLAN Workshop on Generic Programming (WGP)},
 pages        = {1--11},
 doi          = {10.1145/2502488.2502491},
)
@article(Mendler91,
 author       = {N. P. Mendler},
 year         = {1991},
 title        = {Inductive Types and Type Constraints in the Second-Order lambda Calculus},
 journal      = {Ann. Pure Appl. Logic},
 volume       = {51},
 number       = {1-2},
 pages        = {159--172},
 doi          = {10.1016/0168-0072(91)90069-X},
)
@inproceedings(PfenningP89,
 author       = {F. Pfenning and Paulin{-}Mohring, C.},
 year         = {1989},
 title        = {Inductively Defined Types in the Calculus of Constructions},
 booktitle    = {Math. Foundations of Programming Semantics},
 pages        = {209--228},
 doi          = {10.1007/BFb0040259},
)
@article(Plotkin04a,
 author       = {G. D. Plotkin},
 year         = {2004},
 title        = {A structural approach to operational semantics},
 journal      = {J. Log. Algebr. Program.},
 volume       = {60-61},
 pages        = {17--139},
 doi          = {10.1016/j.jlap.2004.03.009},
)
@article(OTT,
 author       = {P. Sewell and Zappa Nardelli, F. and S. Owens and G. Peskine and T. Ridge and S. Sarkar and Strni\v{s}a, R.},
 year         = {2010},
 title        = {Ott: Effective Tool Support for the Working Semanticist},
 journal      = {Journal of Functional Programming},
 volume       = {20},
 number       = {1},
 pages        = {71--122},
 doi          = {10.1017/S0956796809990293},
)
@article(Swier08,
 author       = {W. Swierstra},
 year         = {2008},
 title        = {Data types {\`{a}} la carte},
 journal      = {Journal of Functional Programming},
 volume       = {18},
 number       = {4},
 pages        = {423--436},
 doi          = {10.1017/S0956796808006758},
)
@unpublished(MACoq,
 author       = {P. Torrini},
 year         = {2015},
 title        = {Language specification and type preservation proofs in {C}oq -- companion code},
 url          = {http://cs.swan.ac.uk/~cspt/MDTC},
)
@article(UustaluV99,
 author       = {T. Uustalu and V. Vene},
 year         = {1999},
 title        = {Mendler-Style Inductive Types, Categorically},
 journal      = {Nord. J. Comput.},
 volume       = {6},
 number       = {3},
 pages        = {343},
)
@unpublished(WadlerRecTypes,
 author       = {P. Wadler},
 year         = {1990},
 title        = {Recursive types for free!},
 url          = {http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt},
)