The Nuprl Open Logical Environment, Automated Deduction-CADE-17, 17th International Conference on Automated Deduction, vol.1831, pp.170-176, 2000. ,
Extensional equality in intensional type theory, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158, pp.412-420, 1999. ,
DOI : 10.1109/lics.1999.782636
URL : http://www.cs.nott.ac.uk/~txa/publ/lics99.pdf
Extending Homotopy Type Theory with Strict Equality, 2016. ,
Observational equality, now!, Proceedings of the 2007 workshop on Programming languages meets program verification, pp.57-68, 2007. ,
DOI : 10.1145/1292597.1292608
URL : http://strictlypositive.org/obseqnow.pdf
Towards Certified Meta-Programming with Typed Template-Coq, Interactive Theorem Proving-9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC, vol.10895, pp.20-39, 2018. ,
DOI : 10.1007/978-3-319-94821-8_2
URL : https://hal.archives-ouvertes.fr/hal-01809681
Two-Level Type Theory and Applications, 2017. ,
The 'Andromeda' prover, 2016. ,
Proofs for free: Parametricity for dependent types, Journal of Functional Programming, vol.22, pp.107-152, 2012. ,
DOI : 10.1145/1863543.1863592
URL : http://www.soi.city.ac.uk/~ross/papers/pts.pdf
Interactive Theorem Proving and Program Development, 2004. ,
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237
A Model of Type Theory in Cubical Sets, 2013. ,
The Next 700 Syntactical Models of Type Theory, Certified Programs and Proofs-CPP 2017, pp.182-194, 2017. ,
DOI : 10.1145/3018610.3018620
URL : https://hal.archives-ouvertes.fr/hal-01445835
, The Coq proof assistant reference manual, 2017.
Conservativity of equality reflection over intensional type theory, International Workshop on Types for Proofs and Programs, pp.153-164, 1995. ,
Extensional constructs in intensional type theory, 1997. ,
The Groupoid Interpretation of Type Theory, Twenty-five years of constructive type theory, vol.36, pp.83-111, 1995. ,
Coq without Type Casts: A Complete Proof of Coq Modulo Theory, LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, vol.46, pp.474-489, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01664457
The simplicial model of univalent foundations, 2012. ,
Dependently typed functional programs and their proofs, 2000. ,
Epigram: Practical programming with dependent types, International School on Advanced Functional Programming, pp.130-170, 2004. ,
Towards a practical programming language based on dependent type theory, vol.32, 2007. ,
Extensionality in the calculus of constructions, International Conference on Theorem Proving in Higher Order Logics, pp.278-293, 2005. ,
Egalité et filtrage avec types dépendants dans le calcul des constructions inductives, Ph.D. Dissertation, 2006. ,
Program-ing Finger Trees in Coq, ICFP'07, pp.13-24, 2007. ,
Equations: A Dependent Pattern-Matching Compiler, Interactive Theorem Proving, First International Conference, ITP 2010, vol.6172, pp.419-434, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00628862
Investigations into intensional type theory, 1993. ,
, The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013.
Explicit convertibility proofs in pure type systems, Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & metalanguages: theory & practice. ACM, pp.25-36, 2013. ,
A simple type system with two identity types, 2013. ,