J. Adámek, Free algebras and automata realizations in the language of categories, Commentationes Mathematicae Universitatis Carolinae, vol.015, pp.589-602, 1974.

B. Ahrens, K. Kapulkin, and M. Shulman, Univalent categories and the Rezk completion, Math. Struct. in Comp. Science, vol.25, pp.1010-1039, 2015.

B. Ahrens and R. Matthes, Heterogeneous substitution systems revisited, 2016.

B. Ahrens and J. Zsidó, Initial Semantics for higher-order typed syntax in Coq, Journal of Formalized Reasoning, vol.4, issue.1, pp.25-69, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01329572

T. Altenkirch and B. Reus, Monadic presentations of lambda terms using generalized inductive types, Computer Science Logic, 13th International Workshop, pp.453-468, 1999.

S. Awodey, N. Gambino, and K. Sojakova, Inductive Types in Homotopy Type Theory, Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, pp.95-104, 2012.

F. Bellegarde and J. Hook, Substitution: A formal methods case study using monads and transformations, Science of Computer Programming, vol.23, pp.287-311, 1994.

R. Bird and L. Meertens, Nested Datatypes, Mathematics of Program Construction, MPC'98, Proceedings, vol.1422, pp.52-67, 1998.

R. S. Bird and R. Paterson, De Bruijn Notation as a Nested Datatype, J. Funct. Program, vol.9, issue.1, pp.77-91, 1999.

R. S. Bird and R. Paterson, Generalised folds for nested datatypes, Formal Asp. Comput, vol.11, issue.2, pp.200-222, 1999.

J. Cartmell, Generalised algebraic theories and contextual categories, Ann. Pure Appl. Logic, vol.32, pp.209-243, 1986.

L. Chicli, L. Pottier, and C. Simpson, Mathematical Quotients and Quotient Types in Coq, Second International Workshop, TYPES 2002, vol.2646, pp.95-107, 2002.

C. Cohen, T. Coquand, S. Huber, and A. Mörtberg, Cubical Type Theory: a constructive interpretation of the univalence axiom, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01378906

M. Fiore, G. Plotkin, and D. Turi, Abstract Syntax and Variable Binding, Proceedings of the IEEE Symposium on Logic in Computer Science, LICS '99, pp.193-202, 1999.

G. Gonthier, A. Mahboubi, and E. Tassi, A Small Scale Reflection Extension for the Coq system, 2016.
URL : https://hal.archives-ouvertes.fr/inria-00258384

M. Hedberg, A Coherence Theorem for Martin-Löf's Type Theory, J. Funct. Program, vol.8, issue.4, pp.413-436, 1998.

A. Hirschowitz and M. Maggesi, Modules over Monads and Linearity, Lecture Notes in Computer Science, vol.4576, pp.218-237, 2007.

A. Hirschowitz and M. Maggesi, Modules over monads and initial semantics, Inf. Comput, vol.208, issue.5, pp.545-564, 2010.

S. Lane, Categories for the Working Mathematician, Graduate Texts in Mathematics, vol.5, 1998.

P. Martin-löf, Constructive mathematics and computer programming, Logic, Methodology and Philosophy of Science VI, vol.104, pp.153-175, 1982.

P. Martin-löf, Intuitionistic Type Theory, Studies in Proof Theory. Bibliopolis, vol.1, 1984.

R. Matthes and T. Uustalu, Substitution in non-wellfounded syntax with variable binding, Theor. Comput. Sci, vol.327, issue.1-2, pp.155-174, 2004.
DOI : 10.1016/s1571-0661(04)80639-x
URL : https://doi.org/10.1016/s1571-0661(04)80639-x

P. Nax and . Mendler, Inductive types and type constraints in the second-order lambda calculus, Ann. Pure Appl. Logic, vol.51, issue.1-2, pp.159-172, 1991.

F. Métayer, Fixed points of functors

, The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics, 2013.

V. Voevodsky, C-system of a module over a monad on sets, 2014.

V. Voevodsky, A C-system defined by a universe category, Theory Appl. Categ, vol.30, issue.37, pp.1181-1215, 2015.

V. Voevodsky, An experimental library of formalized mathematics based on the univalent foundations, Mathematical Structures in Computer Science, vol.25, pp.1278-1294, 2015.