D. Andler and R. Et-martin, Logique mathématique. Encyclopaedia Universalis, p.14, 1984.

J. Avigad and S. Et-feferman, The Handbook of Proof Theory, chapitre Gödel's functional ("Dialectica") interpretation, pp.337-405, 1998.

H. Barendregt, Introduction to generalized type systems, Journal of Functional Programming, vol.1, issue.2, pp.125-154, 1991.

H. Barendregt, Lambda calculi with types, volume 2 de Handbook of Logic in Computer Science, pp.117-309, 1992.

B. Barras, Coq en coq, 1996.
URL : https://hal.archives-ouvertes.fr/inria-00073667

C. Böhm and A. Et-berarducci, 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. Church, 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

L. Colson, Quelques remarques sur l'environnement dans la Théorie Intuitionniste des Types, 1986.

L. Colson and D. Michel, Pedagogical natural deduction systems : the propositional case, Journal of Universal Computer Science, vol.13, issue.10, pp.1396-1410, 2007.

L. Colson and D. Michel, Pedagogical Second-order Propositional Calculi, Journal of Logic and Computation, vol.11, issue.4, pp.669-695, 2008.
DOI : 10.1093/logcom/exn001

L. Colson and D. Michel, 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

T. Coquand, Une théorie des constructions, Thèse de doctorat, 1985.

N. De-bruijn, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, 1972.

N. G. De-bruijn, D. Lacombe, L. Nolin, and M. Et-schützenberger, The mathematical language AUTOMATH, its usage, and some of its extensions, éditeurs : Symposium on Automatic Demonstration, pp.29-61, 1970.
DOI : 10.1007/BFb0060623

N. G. De-bruijn, J. P. Seldin, and J. R. Et-hindley, A survey of the projet Automath, éditeurs : To H. B. Curry : Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp.579-606, 1980.

G. Dowek, 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

S. Feferman, J. Dawson, J. W. Kleene, S. C. Moore, G. H. Solovay et al., Kurt Gödel : collected works, pp.1938-1974, 1990.

M. Franchella, Brouwer and griss on intuitionistic negation, Modern Logic, vol.4, issue.3, pp.256-265, 1994.

H. Friedman, Classically and intuitionistically provably recursive functions, pp.21-27, 1978.
DOI : 10.1007/BFb0103100

P. Gilmore, 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.

J. Girard, Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur, Thèse de doctorat d'état, 1972.

J. Girard, P. Taylor, and Y. Et-lafont, Proofs and types, 1990.

G. Griss, Negationless intuitionistic mathematics, Indagationes Mathematicae, vol.8, pp.675-681, 1946.
DOI : 10.1016/s1385-7258(51)50064-1

G. Griss, Negationless intuitionistic mathematics II, Indagationes Mathematicae, vol.12, pp.108-115, 1950.
DOI : 10.1016/s1385-7258(51)50027-6

G. Griss, Negationless Intuitionistic Mathematics. III, Indagationes Mathematicae (Proceedings), vol.54, pp.193-199, 1951.
DOI : 10.1016/S1385-7258(51)50027-6

G. Griss, Negationless Intuitionistic Mathematics. IVa, Indagationes Mathematicae (Proceedings), vol.54, pp.452-462463, 1951.
DOI : 10.1016/S1385-7258(51)50064-1

V. K. Gödel, Über eine bisher noch nicht benÜtzte erweiterung des finiten standpunktes, Dialectica, vol.12, pp.3-4280, 1958.

A. Heyting, G. F. C. Griss and his negationless intuitionistic mathematics, Synthese, vol.56, issue.1, pp.91-96, 1955.
DOI : 10.1007/BF00567395

W. A. Howard, The formulas-as-types notion of construction, éditeurs : To H. B. Curry : Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp.479-490, 1980.

G. W. Huet, The Constructive Engine éditeur : A Perspective in Theoretical Computer Science ? Commemorative Volume for Gift Siromoney, pp.38-69, 1989.

S. C. Kleene, 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

V. N. Krivtsov, A Negationless Interpretation of Intuitionistic Theories. I. Studia Logica, pp.323-344, 2000.

V. N. Krivtsov, A Negationless Interpretation of Intuitionistic Theories. II, Studia Logica, vol.65, issue.2, pp.155-179, 2000.
DOI : 10.1023/A:1005207512630

E. G. López-escobar, Constructions and negationless logic, Studia Logica, vol.11, issue.1, pp.7-22, 1972.
DOI : 10.1007/BF02120815

E. G. López-escobar, Elementary interpretations of negationless arithmetic, Fundamenta Mathematicae, vol.82, issue.1, pp.25-38, 1974.
DOI : 10.4064/fm-82-1-25-38

Z. Luo, ECC, an extended calculus of constructions, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, 1990.
DOI : 10.1109/LICS.1989.39193

P. Martin-löf, A theory of types, 1971.

V. Mezhlumbekova, Deductive capabilities of negationless intuitionistic arithmetic, Moscow University Mathematical Bulletin, vol.30, issue.2, 1975.

D. Michel, Systèmes formels et systèmes fonctionnels pédagogiques, Thèse de doctorat, 2008.

J. K. Minichiello, An extension of negationless logic., Notre Dame Journal of Formal Logic, vol.10, issue.3, pp.298-302, 1969.
DOI : 10.1305/ndjfl/1093893719

G. Mints, Notes on Constructive Negation, Synthese, vol.52, issue.3, pp.701-717, 2006.
DOI : 10.1007/978-1-4613-0609-2_1

D. Nelson, Non-null implication, The Journal of Symbolic Logic, vol.11, issue.04, pp.562-572, 1966.
DOI : 10.1090/S0002-9947-1947-0025420-1

D. Nelson, A complete negationless system, Studia Logica, vol.31, issue.1, pp.41-49, 1973.
DOI : 10.1007/978-3-642-86718-7

J. Reynolds and B. Robinet, Towards a theory of type structure, éditeur : Programming Symposium, pp.408-425, 1974.
DOI : 10.1007/3-540-06859-7_148

M. H. Sørensen and P. Et-urzyczyn, Lectures on the Curry-Howard Isomorphism, de Studies in Logic and the Foundations of Mathematics, 2006.

P. Urzyczyn, P. De-groote, and J. Et-roger-hindley, 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

V. Valpola, Ein system der negationlosen Logik mit ausschliesslich realisierbaren Prädicaten, Acta Philosophica Fennica, vol.9, pp.1-247, 1955.

D. T. Van-daalen, R. P. Nederpelt, J. H. Geuvers, R. C. Et-de-vrijer, and . Éditeurs, Selected papers on Automath, de Studies in Logic and the Foundations of Mathematics, pp.101-126, 1994.

P. Vredenduin, The logic of negationless mathematics, Compositio Mathematica, vol.11, pp.204-277, 1953.