Algorithmic Equality in Heyting Arithmetic Modulo, TYPES, 2007. ,
DOI : 10.1007/978-3-540-68103-8_1
Definitions by rewriting in the calculus of constructions, Logic in Computer Science, pp.9-18, 2001. ,
URL : https://hal.archives-ouvertes.fr/inria-00105568
Inductive Types in the Calculus of Algebraic Constructions, 2003. ,
DOI : 10.1007/3-540-44904-3_4
URL : https://hal.archives-ouvertes.fr/inria-00105617
Normalization in supernatural deduction and in deduction modulo, 2007. ,
URL : https://hal.archives-ouvertes.fr/inria-00141720
Principles of Superdeduction, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pp.41-50, 2007. ,
DOI : 10.1109/LICS.2007.37
URL : https://hal.archives-ouvertes.fr/inria-00133557
Towards Rewriting in Coq, Rewriting, Computation and Proof, pp.113-131, 2007. ,
DOI : 10.1007/978-3-540-73147-4_6
The rewriting calculus - part II, Logic Journal of IGPL, vol.9, issue.3, pp.427-498, 2001. ,
DOI : 10.1093/jigpal/9.3.377
URL : https://hal.archives-ouvertes.fr/inria-00100532
Rewriting Calculus with Fixpoints: Untyped and First-Order Systems, Proceedings of TYPES, 2003. ,
DOI : 10.1007/978-3-540-24849-1_10
URL : https://hal.archives-ouvertes.fr/inria-00100113
Completeness and Cut-elimination in the Intuitionistic Theory of Types, Journal of Logic and Computation, vol.15, issue.6, pp.821-854, 2005. ,
DOI : 10.1093/logcom/exi055
Truth Values Algebras and Proof Normalization, TYPES, pp.110-124, 2006. ,
DOI : 10.1007/978-3-540-74464-1_8
Theorem proving modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003. ,
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/hal-01199506
Cut elimination for zermelo's set theory. Available on author's web page ,
Abstract, The Journal of Symbolic Logic, vol.87, issue.04, pp.1289-1316, 2003. ,
DOI : 10.1007/BFb0037116
Arithmetic as a Theory Modulo ,
DOI : 10.1007/978-3-540-32033-3_31
UntersuchungenüberUntersuchungen¨Untersuchungenüber das logische schließen, Logik-Texte: Kommentierte Auswahl zur Geschichte der Modernen Logik (vierte Auflage), pp.206-262, 1986. ,
A tutorial on recursive types in coq, 1998. ,
URL : https://hal.archives-ouvertes.fr/inria-00069950
Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science, 1989. ,
Semantic Cut Elimination in the Intuitionistic Sequent Calculus, Typed Lambda- Calculi and Applications, pp.221-233, 2005. ,
DOI : 10.1007/11417170_17
Cohérence de la déduction surnaturelle, 2006. ,
A Finite First-Order Theory of Classes, Proc. 2006 Int. Workshop on Proofs and Programs, Lecture notes in Computer Science, 2006. ,
DOI : 10.1007/978-3-540-74464-1_13
A uniform semantic proof for cut-elimination and completeness of various first and higher order logics, Theoretical Computer Science, vol.281, issue.1-2, pp.471-498, 2002. ,
DOI : 10.1016/S0304-3975(02)00024-5
Programming with proofs: A second order type theory, ESOP '88: Proceedings of the 2nd European Symposium on Programming, pp.145-159, 1988. ,
DOI : 10.1007/3-540-19027-9_10
Inductive definitions in the system Coq rules and properties, TLCA '93: Proceedings of the International Conference on Typed Lambda Calculi and Applications, pp.328-345, 1993. ,
DOI : 10.1007/BFb0037116
Resolution in type theory, pp.414-432, 1971. ,
Hauptsatz for higher order logic, The Journal of Symbolic Logic, vol.25, issue.03, pp.452-457, 1968. ,
DOI : 10.1090/S0002-9904-1966-11611-7
Intensional interpretation of functionals of finite type I. jsl, pp.198-212, 1967. ,
A proof of cut-elimination theorem in simple type-theory, Journal of the Mathematical Society of Japan, vol.19, issue.4, pp.399-410, 1967. ,
DOI : 10.2969/jmsj/01940399
Une Théorie des Constructions Inductives, 1994. ,