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.
H. Barendregt (1992):
Lambda Calculi with Types.
In: Hand. of Logic in Co. Sc..
Oxford,
pp. 117–309.
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.
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.
T. Coquand & G. Huet (1988):
The calculus of constructions.
Information and Computation 76,
pp. 95–120,
doi:10.1016/0890-5401(88)90005-3.
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.
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.
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.
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.
G. Hutton (1999):
A Tutorial on the Universality and Expressiveness of Fold.
J. Funct. Program. 9(4),
pp. 355–372,
doi:10.1017/S0956796899003500.
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.
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.
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.
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.
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.
W. Swierstra (2008):
Data types à la carte.
Journal of Functional Programming 18(4),
pp. 423–436,
doi:10.1017/S0956796808006758.
P. Torrini (2015):
Language specification and type preservation proofs in Coq – companion code.
Available at http://cs.swan.ac.uk/~cspt/MDTC.
T. Uustalu & V. Vene (1999):
Mendler-Style Inductive Types, Categorically.
Nord. J. Comput. 6(3),
pp. 343.
eptcs@eptcs.org