Decidability of Conversion for Type Theory in Type Theory, Proceedings of the ACM on Programming Languages 2, POPL, vol.29, p.23, 2018. ,
Higher-Order Dynamic Pattern Unification for Dependent Types and Records, Typed Lambda Calculi and Applications -10th International Conference, vol.6690, pp.10-26, 2011. ,
New Equations for Neutral Terms: A Sound and Complete Decision Procedure, Formalized, Proceedings of the 2013 ACM SIGPLAN Workshop on Dependently-typed Programming (DTP '13), pp.13-24, 2013. ,
Higher-Order (Non-)Modularity, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, vol.6, pp.17-32, 2010. ,
Translating HOL to Dedukti, Electronic Proceedings in Theoretical Computer Science, vol.186, pp.74-88, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01097412
Modularity of Strong Normalization in the Algebraiclambda-Cube, Journal of Functional Programming, vol.7, pp.613-660, 1997. ,
The Lambda Calculus, Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, vol.103, 1984. ,
CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory, Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, pp.143-151, 2011. ,
URL : https://hal.archives-ouvertes.fr/inria-00583136
Martin Hofmann's Case for Non-Strictly Positive Data Types, 24th International Conference on Types for Proofs and Programs, vol.130, pp.1-1, 2018. ,
A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems, Rewriting Techniques and Applications, 15th International Conference, vol.3091, pp.24-39, 2004. ,
URL : https://hal.archives-ouvertes.fr/inria-00100254
Definitions by rewriting in the Calculus of Constructions, Mathematical Structures in Computer Science, vol.15, pp.37-92, 2005. ,
URL : https://hal.archives-ouvertes.fr/inria-00105648
Size-based termination of higher-order rewriting, Journal of Functional Programming, vol.28, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01424921
Type Safety of Rewrite Rules in Dependent Types, 5th International Conference on Formal Structures for Computation and Deduction, vol.2020, pp.1-13, 2020. ,
The Computability Path Ordering: The End of a Quest, Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, vol.5213, pp.1-14, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00288209
The ??-calculus Modulo as a Universal Proof Language, the Second International Workshop on Proof Exchange for Theorem Proving, vol.878, pp.28-43, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00917845
Towards Rewriting in Coq, Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, vol.4600, pp.113-131, 2007. ,
Type theory unchained: Extending Agda with user-defined rewrite rules (system description), 2020. ,
, The Coq proof assistant reference manual, 2016.
Inductively Defined Types, Proceedings of the International Conference on Computer Logic (COLOG '88), pp.50-66, 1988. ,
Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, Typed Lambda Calculi and Applications, 8th International Conference, vol.4583, pp.102-117, 2007. ,
Proof Orders for Decreasing Diagrams, 24th International Conference on Rewriting Techniques and Applications, RTA 2013, vol.21, pp.174-189, 2013. ,
Confluence in (Un)Typed Higher-Order Theories by means of Critical Pairs, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-02096540
SizeChangeTool: A Termination Checker for Rewriting Dependent Types, HOR 2019 -10th International Workshop on Higher-Order Rewriting (Joint Proceedings of HOR 2019 and IWC 2019), pp.14-19, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-02442465
Definitional Proof-Irrelevance without K, Proceedings of the ACM on Programming Languages, vol.3, pp.1-28, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-01859964
Non Strictly Positive Datatypes in System F. Email on types mailing list, 1993. ,
Termination of Dependently Typed Rewrite Rules, 13th International Conference on Typed Lambda Calculi and Applications, vol.38, pp.257-272, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01239083
A Computation Model for Executable Higher-Order Algebraic Specification Languages, Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, pp.350-361, 1991. ,
The Higher-Order Recursive Path Ordering, Proceedings, 14th Annual IEEE Symposium on Logic in Computer Science, pp.402-411, 1999. ,
Coq without Type Casts: A Complete Proof of Coq Modulo Theory, LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EasyChair, pp.474-489, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01664457
The size-change principle for program termination, Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.81-92, 2001. ,
Confluence properties of rewrite rules by decreasing diagrams. (Propriétés de confluence des règles de réécriture par des diagrammes décroissants), 2016. ,
URL : https://hal.archives-ouvertes.fr/tel-01515698
An Intuitionistic Theory of Types: Predicative Part, Studies in Logic and the Foundations of Mathematics, vol.80, pp.71945-71946, 1975. ,
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
Failure is Not an Option: An Exceptional Type Theory, ESOP 2018 -27th European Symposium on Programming, vol.10801, pp.245-271, 2018. ,
A Reasonably Exceptional Type Theory, Proceedings of the ACM on Programming Languages 3, ICFP, Article, vol.108, 2019. ,
Typechecking in the lambda-Pi-Calculus Modulo: Theory and Practice, Ph.D. Dissertation. MINES ParisTech, 2015. ,
URL : https://hal.archives-ouvertes.fr/tel-01299180
Confluence and Normalization in Reduction Systems, 2015. ,
The MetaCoq Project, Journal of Automated Reasoning, 2020. ,
URL : https://hal.archives-ouvertes.fr/hal-02167423
Coq Coq Correct! Verification of Type Checking and Erasure for Coq, Coq. Proceedings of the ACM on Programming Languages 4, POPL, Article, vol.8, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-02380196
The Open Calculus of Constructions (Part I): An Equational Type Theory with Dependent Types for Programming, Specification, and Interactive Theorem Proving, Fundamenta Informaticae, vol.68, pp.131-174, 2005. ,
The Open Calculus of Constructions (Part II): An Equational Type Theory with Dependent Types for Programming, Specification, and Interactive Theorem Proving, Fundamenta Informaticae, vol.68, pp.249-288, 2005. ,
Coq Modulo Theory, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, vol.6247, pp.529-543, 2010. ,
URL : https://hal.archives-ouvertes.fr/inria-00497404
Parallel Reductions in ?-Calculus, Information and Computation, vol.118, pp.120-127, 1995. ,
Combining Algebra and Higher-Order Types, Proceedings, Third Annual Symposium on Logic in Computer Science, pp.82-90, 1988. ,
Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, vol.55, 2003. ,
, The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study
Confluence by Decreasing Diagrams, Theoretical Computer Science, vol.126, pp.259-280, 1994. ,
Confluence for abstract and higher-order rewriting, 1994. ,
Selected Papers (Lecture Notes in Computer Science), Gilles Dowek, Higher-Order Algebra, Logic, and Term Rewriting, Second International Workshop, HOA '95, vol.1074, pp.185-200, 1995. ,
Termination of rewriting in the Calculus of Constructions, Journal of Functional Programming, vol.13, pp.339-414, 2003. ,
Consistency and Completeness of Rewriting in the Calculus of Constructions, Automated Reasoning, Third International Joint Conference, vol.4130, pp.619-631, 2006. ,