Semi-continuous Sized Types and Termination, Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, vol.4207, pp.72-88, 2006. ,
DOI : 10.1007/11874683_5
URL : http://arxiv.org/pdf/0804.0876v1.pdf
Well-founded recursion with copatterns and sized types, J. Funct. Program, vol.26, 2016. ,
Observational Equality, Now!, PLPV'07, 2007. ,
DOI : 10.1145/1292597.1292608
URL : http://strictlypositive.org/obseqnow.pdf
Partiality and recursion in interactive theorem provers-an overview, Mathematical Structures in Computer Science FirstView, pp.1-51, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-00691459
CertiCoq: A verified compiler for Coq, CoqPL, 2017. ,
The Lean Reference Manual, 2017. ,
Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. Functional and Logic Programming, pp.114-129, 2006. ,
URL : https://hal.archives-ouvertes.fr/inria-00564237
The HoTT Library: A formalization of homotopy type theory in Coq, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01421212
Guarded Cubical Type Theory: Path Equality for Guarded Recursion, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, vol.62, pp.1-23, 2016. ,
DOI : 10.1007/s10817-018-9471-7
URL : http://arxiv.org/pdf/1611.09263
Dependent Pattern Matching and Proof-Relevant Unification, Ph.D. Dissertation. Katholieke Universiteit Leuven, 2017. ,
Lifting proof-relevant unification to higher dimensions, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, pp.173-181, 2017. ,
DOI : 10.1145/3018610.3018612
Pattern matching without K, Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, pp.257-268, 2014. ,
DOI : 10.1145/2628136.2628139
Cubical Type Theory: a constructive interpretation of the univalence axiom, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01378906
Pattern Matching with Dependent Types, Proceedings of the Workshop on Logical Frameworks, 1992. ,
Eliminating Dependent Pattern Matching, Essays Dedicated to Joseph A. Goguen (Lecture Notes in Computer Science), vol.4060, pp.521-540, 2006. ,
DOI : 10.1007/11780274_27
A Groupoid Model Refutes Uniqueness of Identity Proofs, LICS, pp.208-212, 1994. ,
DOI : 10.1109/lics.1994.316071
Generalizations of Hedberg's Theorem, Lecture Notes in Computer Science, vol.7941, pp.173-188, 2013. ,
DOI : 10.1007/978-3-642-38946-7_14
URL : http://www.cs.bham.ac.uk/~mhe/papers/hedberg.pdf
Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq, Ph.D. Dissertation. University of Paris-Sud, 2011. ,
URL : https://hal.archives-ouvertes.fr/tel-00713668
Weak omega-categories from intensional type theory, Logical Methods in Computer Science, vol.6, p.3, 2010. ,
Equations for Hereditary Substitution in Leivant's Predicative System F: A Case Study, Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice (EPTCS), vol.185, 2015. ,
DOI : 10.4204/eptcs.185.5
URL : http://arxiv.org/pdf/1508.00455
Intuitionistic type theory, Studies in Proof Theory, vol.1, 1984. ,
Dependently Typed Functional Programs and Their Proofs, Ph.D. Dissertation. University of Edinburgh, 1999. ,
Elimination with a Motive, TYPES (Lecture Notes in Computer Science), vol.2277, pp.197-216, 2000. ,
, A Few Constructions on Constructors. Types for Proofs and Programs, pp.186-200, 2004.
Handcrafted Inversions Made Operational on Operational Semantics, pp.338-353, 2013. ,
DOI : 10.1007/978-3-642-39634-2_25
URL : https://hal.archives-ouvertes.fr/hal-00937168
Towards a practical programming language based on dependent type theory, 2007. ,
Inductive Definitions in the System Coq-Rules and Properties, Typed Lambda Calculi and Applications, vol.664, pp.328-345, 1993. ,
DOI : 10.1007/bfb0037116
Homotopy type theory and Voevodsky's univalent foundations, 2012. ,
DOI : 10.1090/s0273-0979-2014-01456-9
URL : https://www.ams.org/bull/2014-51-04/S0273-0979-2014-01456-9/S0273-0979-2014-01456-9.pdf
Program-ing Finger Trees in Coq, ICFP'07, pp.13-24, 2007. ,
Equations: A Dependent Pattern-Matching Compiler, First International Conference on Interactive Theorem Proving, 2010. ,
DOI : 10.1007/978-3-642-14052-5_29
URL : https://hal.archives-ouvertes.fr/inria-00628862
Total Haskell is reasonable Coq, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp.14-27, 2018. ,
DOI : 10.1145/3176245.3167092
URL : http://arxiv.org/pdf/1711.09286
, The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations for Mathematics. Institute for Advanced Study
Types are weak ?-groupoids, Proceedings of the London Mathematical Society, vol.102, pp.370-394, 2011. ,