Observational equality, now!, Proceedings of the Workshop on Programming Languages meets Program Verification, pp.57-68, 2007. ,
Revisiting Parametricity: Inductives and Uniformity of Propositions, 2017. ,
The Untenability of Genera, Logique et Analyse, vol.17, pp.197-208, 1974. ,
The HoTT Library: A Formalization of Homotopy Type Theory in Coq, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, pp.164-172, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01421212
A Presheaf Model of Parametric Type Theory, Electronic Notes in Theoretical Computer Science, vol.319, pp.67-82, 2015. ,
Proofs for free: Parametricity for dependent types, Journal of Functional Programming, vol.22, issue.2, pp.107-152, 2012. ,
The next 700 syntactical models of type theory, Certified Programs and Proofs, pp.182-194, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01445835
Cubical Type Theory: a constructive interpretation of the univalence axiom, vol.262, p.29, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01378906
Refinements for Free!, Proceedings of the International Conference on Certified Programming and Proofs (CPP 2013) (Lecture Notes in Computer Science, vol.8307, pp.147-162, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-01113453
, The Coq proof assistant reference manual, 2019.
Wellfounded trees and dependent polynomial functors, Proceedings of Types for Proofs and Programs (TYPES 2003), vol.3085, pp.210-225, 2004. ,
Data Refinement in Isabelle/HOL, Proceedings of the 4th International Conference on Interactive Theorem Proving (ITP 2013) (Lecture Notes in Computer Science), vol.7998, pp.100-115, 2013. ,
Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL, Proceedings of the 3rd International Conference on Certified Programs and Proofs, pp.131-146, 2013. ,
Internalizing Relational Parametricity in the Extensional Calculus of Constructions, Proceedings of the Conference for Computer Science Logic (CSL 2013, pp.432-451, 2013. ,
Automatic Data Refinement, Proceedings of the 4th International Conference on Interactive Theorem Proving (ITP 2013) (Lecture Notes in Computer Science), vol.7998, pp.84-99, 2013. ,
Changing Data Representation within the Coq system, International Conference on Theorem Proving in Higher Order Logics, vol.2758, 2003. ,
Changing Data Structures in Type Theory: A Study of Natural Numbers, International Workshop on Types for Proofs and Programs (TYPES 2000) (Lecture Notes in Computer Science), vol.2277, pp.181-196, 2000. ,
An Intuitionistic Theory of Types, 1971. ,
Introduction to the Calculus of Inductive Constructions, Studies in Logic (Mathematical logic and foundations), vol.55, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01094195
Simple unification-based type inference for GADTs, Proceedings of the 11th ACM SIGPLAN Conference on Functional Programming, pp.50-61, 2006. ,
Types, Abstraction and Parametric Polymorphism, IFIP Congress, pp.513-523, 1983. ,
First-Class Type Classes, Proceedings of the 21st International Conference on Theorem Proving in Higher-Order Logics, pp.278-293, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00628864
, The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013.
Theorems for Free!. In Functional Programming Languages and Computer Architecture, pp.347-359, 1989. ,
Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01152588