, Proving strong normalization of CC by modifying realizability semantics, Lecture Notes in Computer Science, vol.806, pp.3-18, 1993.
DOI : 10.1007/3-540-58085-9_70
URL : ftp://ftp.cs.chalmers.se/pub/users/alti/bra-rev.ps
, A calculus of constructions with explicit subtyping, 20th International Conference on Types for Proofs and Programs, TYPES 2014 Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.27-46, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01097401
, Untyped confluence in dependent type theory, 2017.
, Semantical Investigations in Intuitionistic Set Theory and Type Theories with Inductive Families
, Sets in Coq, Coq in Sets, J. Formalized Reasoning, vol.3, issue.1, pp.29-48, 2010.
, CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory, 2011 IEEE 26th Annual Symposium on Logic in Computer Science, pp.143-151, 2011.
DOI : 10.1109/LICS.2011.37
URL : https://hal.archives-ouvertes.fr/inria-00583136
, Inductive Types in the Calculus of Algebraic Constructions, TLCA, volume 2701 of Lecture Notes in Computer Science, pp.46-59, 2003.
DOI : 10.1007/3-540-44904-3_4
URL : https://hal.archives-ouvertes.fr/inria-00105617
, From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures, IFIP TCS, pp.349-365, 2008.
DOI : 10.1007/978-0-387-09680-3_24
URL : https://hal.archives-ouvertes.fr/inria-00275382
, SPIKE: A system for sufficient completeness and parameterized inductive proofs, 12th International Conference on Automated Deduction Proceedings, pp.836-840, 1994.
DOI : 10.1007/3-540-58156-1_71
, The calculus of constructions, Information and Computation, vol.76, issue.2-3, pp.95-120, 1988.
DOI : 10.1016/0890-5401(88)90005-3
URL : https://hal.archives-ouvertes.fr/inria-00076024
, Rewrite Systems Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics, J. van Leuven, pp.243-320, 1990.
, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM, vol.27, issue.4, pp.797-821, 1980.
DOI : 10.1145/322217.322230
, Completion of a Set of Rules Modulo a Set of Equations, SIAM J. Comput, vol.15, issue.4, pp.1155-1194, 1986.
, Church-Rosser properties of normal rewriting Computer Science Logic (CSL'12) -21st Annual Conference of the EACSL, CSL 2012, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.350-365, 2012.
, ECC, an extended calculus of constructions, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.386-395, 1989.
DOI : 10.1109/LICS.1989.39193
, Constructive Mathematics and Computer Programming, Logic, methodology and philosophy of science VI, Proceedings of the 1979 international congress at, pp.153-175, 1982.
DOI : 10.1016/S0049-237X(09)70189-2
, Extensionality in the Calculus of Constructions, Lecture Notes in Computer Science, vol.3603, pp.278-293, 2005.
DOI : 10.1007/11541868_18
, Inductive definitions in the system Coq rules and properties, Lecture Notes in Computer Science, vol.664, pp.328-345, 1993.
DOI : 10.1007/BFb0037116
, The Open Calculus of Constructions (Part I ): An Equational Type Theory with Dependent Types for Programming, Specification, and Interactive Theorem Proving, Fundam. Inform, vol.68, issue.12, pp.131-174, 2005.
, Coq Modulo Theory, Lecture Notes in Computer Science, vol.6247, pp.529-543, 2010.
DOI : 10.1007/978-3-642-15205-4_40
URL : https://hal.archives-ouvertes.fr/inria-00497404
, Semantics of Intensional Type Theory extended with Decidable Equational Theories, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.653-667, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00937197
, Sets in types, types in sets, TACS, volume 1281 of Lecture Notes in Computer Science, pp.530-346, 1997.
DOI : 10.1007/BFb0014566