, UntersuchungenüberUntersuchungen¨Untersuchungenüber das logische schließen, Logik-Texte: Kommentierte Auswahl zur Geschichte der Modernen Logik (vierte Auflage)
, 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
, 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
, Resolution in type theory, pp.414-432, 1971.
, Semantic Cut Elimination in the Intuitionistic Sequent Calculus, Lecture Notes in Computer Science, vol.3461, pp.221-233, 2005.
DOI : 10.1007/11417170_17
, 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
, 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
, Abstract, The Journal of Symbolic Logic, vol.87, issue.04, pp.1289-1316, 2003.
DOI : 10.1007/BFb0037116
, Algorithmic Equality in Heyting Arithmetic Modulo, In: TYPES, 2007.
DOI : 10.1007/978-3-540-68103-8_1
, Arithmetic as a Theory Modulo, Proceedings of RTA'05, pp.423-437, 2005.
DOI : 10.1007/978-3-540-32033-3_31
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.120.6757
, Intensional interpretations of functionals of finite type I, The Journal of Symbolic Logic, vol.91, issue.02, pp.198-212, 1967.
DOI : 10.1007/BF01447860
, Une Théorie des Constructions Inductives, 1994.
, 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
, A tutorial on recursive types in coq, 1998.
URL : https://hal.archives-ouvertes.fr/inria-00069950
, Towards a practical programming language based on dependent type theory, pp.412-96, 2007.
, Natural Deduction. A Proof-Theoretical Study, Almqvist and Wiksell, 1965.
, About Folding-Unfolding Cuts and Cuts Modulo, Journal of Logic and Computation, vol.11, issue.3, pp.419-429, 2001.
DOI : 10.1093/logcom/11.3.419
URL : https://hal.archives-ouvertes.fr/inria-00072640
, Proofs and Types. Volume 7 of Cambridge Tracts in Theoretical Computer Science, 1989.
, 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
, Proof normalization for a first-order formulation of higher-order logic, LNCS, vol.1275, pp.105-119, 1997.
DOI : 10.1007/BFb0028389
URL : https://hal.archives-ouvertes.fr/inria-00073306
, Natural Deduction, a Proof-theoretical Study, 1965.
, Truth Values Algebras and Proof Normalization, In: TYPES, pp.110-124, 2006.
DOI : 10.1007/978-3-540-74464-1_8
, Programming with proofs: A second order type theory, Proceedings of the 2nd European Symposium on Programming, pp.145-159, 1988.
DOI : 10.1007/3-540-19027-9_10
, 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
, Definitions by rewriting in the calculus of constructions, In: Logic in Computer Science, pp.9-18, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00105568
, Inductive Types in the Calculus of Algebraic Constructions, pp.3-61, 2003.
DOI : 10.1007/3-540-44904-3_4
URL : https://hal.archives-ouvertes.fr/inria-00105617
, An arithmetical proof of the strong normalization results for the lambdacalculus with recursive equations on types, pp.7-84, 2007.
, Classical Logic and Computation, 2000.
, Séquents qu'on calcule, 1995.