An Introduction to Inductive Definitions, Studies in Logic and the Foundations of Mathematics, vol.90, pp.739-782, 1977. ,
On Relating Type Theories and Set Theories, Thorsten Altenkirch, Bernhard Reus, and Wolfgang Naraschewski, pp.1-18, 1999. ,
, Semantical Investigation in Intuitionistic Set Theory and Type Theoris with Inductive Families, 2012.
The Next 700 Syntactical Models of Type Theory, CPP 2017, pp.182-194, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01445835
Set theory : an introduction to large cardinals. Studies in logic and the foundations of mathematics 76, 1974. ,
Inductive Sets and Families in Martin-Löf's Type Theory and Their SetTheoretic Semantics, pp.280-306, 1991. ,
Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur, 1972. ,
Type checking, universe polymorphism, and typical ambiguity in the calculus of constructions draft, TAPSOFT '89, pp.241-256, 1989. ,
A simplification of Girard's paradox, International Conference on Typed Lambda Calculi and Applications, pp.266-278, 1995. ,
Proof-irrelevant model of CC with predicative induction and judgmental equality, Logical Methods in Computer Science, vol.7, issue.4, 2011. ,
Universe hierarchies, 2015. ,
Définitions Inductives en Théorie des Types d'Ordre Supérieur. Habilitation à diriger les recherches, 1996. ,
Dependently typed lambda calculus with a lifting operator, 2014. ,
Pure type system conversion is always typable, J. Funct. Program, vol.22, issue.2, pp.153-180, 2012. ,
URL : https://hal.archives-ouvertes.fr/inria-00497177
Universe Polymorphism in Coq, Interactive Theorem Proving, pp.499-514, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-00974721
, The Coq Development Team. The Coq Proof Assistant, 2017.
First Steps Towards Cumulative Inductive Types in CIC, Theoretical Aspects of Computing, pp.608-617, 2015. ,
Category Theory in Coq 8.5. In Formal Structures for Computation and Deduction, vol.30, 2016. ,
Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC), KU Leuven, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01615123