Logique mathématique. Encyclopaedia Universalis, p.14, 1984. ,
The Handbook of Proof Theory, chapitre Gödel's functional ("Dialectica") interpretation, pp.337-405, 1998. ,
Introduction to generalized type systems, Journal of Functional Programming, vol.1, issue.2, pp.125-154, 1991. ,
Lambda calculi with types, volume 2 de Handbook of Logic in Computer Science, pp.117-309, 1992. ,
Coq en coq, 1996. ,
URL : https://hal.archives-ouvertes.fr/inria-00073667
Automatic synthesis of typed ??-programs on term algebras, Theoretical Computer Science, vol.39, issue.0, pp.135-154, 1985. ,
DOI : 10.1016/0304-3975(85)90135-5
A Set of Postulates For the Foundation of Logic, The Annals of Mathematics, vol.34, issue.4, pp.839-864, 1933. ,
DOI : 10.2307/1968702
Quelques remarques sur l'environnement dans la Théorie Intuitionniste des Types, 1986. ,
Pedagogical natural deduction systems : the propositional case, Journal of Universal Computer Science, vol.13, issue.10, pp.1396-1410, 2007. ,
Pedagogical Second-order Propositional Calculi, Journal of Logic and Computation, vol.11, issue.4, pp.669-695, 2008. ,
DOI : 10.1093/logcom/exn001
Pedagogical second-order <mml:math altimg="si1.gif" display="inline" overflow="scroll" xmlns:xocs="http://www.elsevier.com/xml/xocs/dtd" xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns="http://www.elsevier.com/xml/ja/dtd" xmlns:ja="http://www.elsevier.com/xml/ja/dtd" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:tb="http://www.elsevier.com/xml/common/table/dtd" xmlns:sb="http://www.elsevier.com/xml/common/struct-bib/dtd" xmlns:ce="http://www.elsevier.com/xml/common/dtd" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:cals="http://www.elsevier.com/xml/common/cals/dtd"><mml:mi>??</mml:mi></mml:math>-calculus, Theoretical Computer Science, vol.410, issue.42, pp.4190-4203, 2009. ,
DOI : 10.1016/j.tcs.2009.04.020
Une théorie des constructions, Thèse de doctorat, 1985. ,
Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, 1972. ,
The mathematical language AUTOMATH, its usage, and some of its extensions, éditeurs : Symposium on Automatic Demonstration, pp.29-61, 1970. ,
DOI : 10.1007/BFb0060623
A survey of the projet Automath, éditeurs : To H. B. Curry : Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp.579-606, 1980. ,
A second-order pattern matching algorithm for the cube of typed lambdacalculi, MFCS, pp.151-160, 1991. ,
URL : https://hal.archives-ouvertes.fr/inria-00074975
Kurt Gödel : collected works, pp.1938-1974, 1990. ,
Brouwer and griss on intuitionistic negation, Modern Logic, vol.4, issue.3, pp.256-265, 1994. ,
Classically and intuitionistically provably recursive functions, pp.21-27, 1978. ,
DOI : 10.1007/BFb0103100
The effect of Griss' criticism of the intuitionistic logic on deductive theories formalized within the intuitionistic logic, Indagationes Mathematicae, vol.15, pp.162-174, 1953. ,
Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur, Thèse de doctorat d'état, 1972. ,
Proofs and types, 1990. ,
Negationless intuitionistic mathematics, Indagationes Mathematicae, vol.8, pp.675-681, 1946. ,
DOI : 10.1016/s1385-7258(51)50064-1
Negationless intuitionistic mathematics II, Indagationes Mathematicae, vol.12, pp.108-115, 1950. ,
DOI : 10.1016/s1385-7258(51)50027-6
Negationless Intuitionistic Mathematics. III, Indagationes Mathematicae (Proceedings), vol.54, pp.193-199, 1951. ,
DOI : 10.1016/S1385-7258(51)50027-6
Negationless Intuitionistic Mathematics. IVa, Indagationes Mathematicae (Proceedings), vol.54, pp.452-462463, 1951. ,
DOI : 10.1016/S1385-7258(51)50064-1
Über eine bisher noch nicht benÜtzte erweiterung des finiten standpunktes, Dialectica, vol.12, pp.3-4280, 1958. ,
G. F. C. Griss and his negationless intuitionistic mathematics, Synthese, vol.56, issue.1, pp.91-96, 1955. ,
DOI : 10.1007/BF00567395
The formulas-as-types notion of construction, éditeurs : To H. B. Curry : Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp.479-490, 1980. ,
The Constructive Engine éditeur : A Perspective in Theoretical Computer Science ? Commemorative Volume for Gift Siromoney, pp.38-69, 1989. ,
A Theory of Positive Integers in Formal Logic. Part I, American Journal of Mathematics, vol.57, issue.1, pp.153-173, 1935. ,
DOI : 10.2307/2372027
A Negationless Interpretation of Intuitionistic Theories. I. Studia Logica, pp.323-344, 2000. ,
A Negationless Interpretation of Intuitionistic Theories. II, Studia Logica, vol.65, issue.2, pp.155-179, 2000. ,
DOI : 10.1023/A:1005207512630
Constructions and negationless logic, Studia Logica, vol.11, issue.1, pp.7-22, 1972. ,
DOI : 10.1007/BF02120815
Elementary interpretations of negationless arithmetic, Fundamenta Mathematicae, vol.82, issue.1, pp.25-38, 1974. ,
DOI : 10.4064/fm-82-1-25-38
ECC, an extended calculus of constructions, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, 1990. ,
DOI : 10.1109/LICS.1989.39193
A theory of types, 1971. ,
Deductive capabilities of negationless intuitionistic arithmetic, Moscow University Mathematical Bulletin, vol.30, issue.2, 1975. ,
Systèmes formels et systèmes fonctionnels pédagogiques, Thèse de doctorat, 2008. ,
An extension of negationless logic., Notre Dame Journal of Formal Logic, vol.10, issue.3, pp.298-302, 1969. ,
DOI : 10.1305/ndjfl/1093893719
Notes on Constructive Negation, Synthese, vol.52, issue.3, pp.701-717, 2006. ,
DOI : 10.1007/978-1-4613-0609-2_1
Non-null implication, The Journal of Symbolic Logic, vol.11, issue.04, pp.562-572, 1966. ,
DOI : 10.1090/S0002-9947-1947-0025420-1
A complete negationless system, Studia Logica, vol.31, issue.1, pp.41-49, 1973. ,
DOI : 10.1007/978-3-642-86718-7
Towards a theory of type structure, éditeur : Programming Symposium, pp.408-425, 1974. ,
DOI : 10.1007/3-540-06859-7_148
Lectures on the Curry-Howard Isomorphism, de Studies in Logic and the Foundations of Mathematics, 2006. ,
Inhabitation in typed lambda-calculi (a syntactic approach), éditeurs : Typed Lambda Calculi and Applications, volume 1210 de Lecture Notes in Computer Science, pp.373-389, 1997. ,
DOI : 10.1007/3-540-62688-3_47
Ein system der negationlosen Logik mit ausschliesslich realisierbaren Prädicaten, Acta Philosophica Fennica, vol.9, pp.1-247, 1955. ,
Selected papers on Automath, de Studies in Logic and the Foundations of Mathematics, pp.101-126, 1994. ,
The logic of negationless mathematics, Compositio Mathematica, vol.11, pp.204-277, 1953. ,