, Free algebras and automata realizations in the language of categories, pp.589-602, 1974.
, Univalent categories and the Rezk completion, Mathematical Structures in Computer Science, vol.20, issue.05, pp.1010-1039, 2015.
DOI : 10.1016/j.indag.2013.09.002
, Heterogeneous substitution systems revisited ArXiv e-prints, 2016.
, 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
, Monadic Presentations of Lambda Terms Using Generalized Inductive Types, Computer Science Logic, 13th International Workshop, pp.453-468, 1999.
DOI : 10.1007/3-540-48168-0_32
, Inductive Types in Homotopy Type Theory, 2012 27th Annual IEEE Symposium on Logic in Computer Science, pp.95-104, 2012.
DOI : 10.1109/LICS.2012.21
URL : http://arxiv.org/abs/1201.3898
, Substitution: A formal methods case study using monads and transformations, Science of Computer Programming, vol.23, issue.2-3, pp.287-311, 1994.
DOI : 10.1016/0167-6423(94)00022-0
, Nested Datatypes Mathematics of Program Construction, MPC'98, Proceedings, volume 1422 of Lecture Notes in Computer Science, pp.52-67, 1998.
, De Bruijn Notation as a Nested Datatype, J. Funct. Program, vol.9, issue.1, pp.77-91, 1999.
, Generalised folds for nested datatypes, Formal Asp. Comput, vol.11, issue.2, pp.200-222, 1999.
, Generalised algebraic theories and contextual categories, Annals of Pure and Applied Logic, vol.32, pp.209-243, 1986.
DOI : 10.1016/0168-0072(86)90053-9
URL : http://doi.org/10.1016/0168-0072(86)90053-9
, Mathematical Quotients and Quotient Types in Coq, Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, pp.95-107, 2002.
DOI : 10.1007/3-540-39185-1_6
, Cubical Type Theory: a constructive interpretation of the univalence axiom. ArXiv e-prints, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01378906
, Abstract syntax and variable binding, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.193-202, 1999.
DOI : 10.1109/LICS.1999.782615
, A Small Scale Reflection Extension for the Coq system, 2016.
URL : https://hal.archives-ouvertes.fr/inria-00258384
, A coherence theorem for Martin-L??f's type theory, Journal of Functional Programming, vol.8, issue.4, pp.413-436, 1998.
DOI : 10.1017/S0956796898003153
, Modules over Monads and Linearity, Lecture Notes in Computer Science, vol.4576, pp.218-237, 2007.
DOI : 10.1007/978-3-540-73445-1_16
URL : http://arxiv.org/abs/cs/0608051
, Modules over monads and initial semantics, Information and Computation, vol.208, issue.5, pp.545-564, 2010.
DOI : 10.1016/j.ic.2009.07.003
URL : http://doi.org/10.1016/j.ic.2009.07.003
, Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics, 1998.
, Constructive mathematics and computer programming In Logic, Methodology and Philosophy of Science VI, of Studies in Logic and the Foundations of Mathematics, pp.153-175, 1982.
, Intuitionistic Type Theory, 1984.
, Substitution in non-wellfounded syntax with variable binding, Theoretical Computer Science, vol.327, issue.1-2, pp.155-174, 2004.
DOI : 10.1016/j.tcs.2004.07.025
, Inductive types and type constraints in the second-order lambda calculus, Ann. Pure Appl. Logic, vol.51, issue.12, pp.159-172, 1991.
, Fixed points of functors
, C-system of a module over a monad on sets. ArXiv e-prints, 2014.
, A C-system defined by a universe category, Theory Appl. Categ, vol.30, issue.37, pp.1181-1215, 2015.
, An experimental library of formalized Mathematics based on the univalent foundations, Mathematical Structures in Computer Science, vol.25, issue.05, pp.1278-1294
DOI : 10.1016/0890-5401(88)90005-3