Decidability of Conversion for Type Theory in Type Theory, Proc. ACM Program, vol.23, 2018. ,
On Irrelevance and Algorithmic Equality in Predicative Type Theory, Logical Methods in Computer Science, vol.8, p.1, 2012. ,
Extensional equality in intensional type theory, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158, 1999. ,
Extending Homotopy Type Theory with Strict Equality, CSL, 2016. ,
, , 2004.
, J. Log. and Comput, vol.14, pp.447-471, 2004.
The Next 700 Syntactical Models of Type Theory, Proceedings of Certified Programs and Proofs, pp.182-194, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01445835
Inductive Families Need Not Store Their Indices, Types for Proofs and Programs, pp.115-129, 2004. ,
Models of type theory with strict equality, 2017. ,
Elaborating Dependent (Co)pattern matching, Proceedings of the 23th ACM SIGPLAN Conference on Functional Programming, 2018. ,
Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory, Journal of Functional Programming, vol.28, 2018. ,
Pattern matching without K, In ACM SIGPLAN Notices, vol.49, pp.257-268, 2014. ,
Universe of Bishop sets, 2016. ,
Internal type theory, Types for Proofs and Programs, pp.120-134, 1996. ,
Conservativity of equality reflection over intensional type theory, International Workshop on Types for Proofs and Programs, pp.153-164, 1995. ,
Programmation fonctionnelle certifiée-L'extraction de programmes dans l'assistant Coq, 2004. ,
An Intuitionistic Theory of Types: Predicative Part, Studies in Logic and the Foundations of Mathematics, vol.80, pp.71945-71946, 2018. ,
Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS '01), p.221, 2001. ,
From realizability to induction via dependent intersection, Ann. Pure Appl. Logic, vol.169, pp.637-655, 2018. ,
, The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013.
Resising Rules-their use and semantic justification, 2011. ,
A simple type system with two identity types, 2013. ,
On the Strength of Proof-Irrelevant Type Theories, pp.1-20, 2008. ,