. ??, f : (??.A) ??? par (? i ) et 4

. ??, f : (??.A) ? est dérivable ; ? 2 ? f : ??.A ? 2 ? f U : [?\U ]·A

A. W. Appel, Compiling with Continuations, 1992.
DOI : 10.1017/CBO9780511609619

H. P. Barendregt, Lambda Calculi with Types, Handbook of Logic in Computer Science, vol.2, 1992.
DOI : 10.1017/cbo9781139032636

A. Church, A Set of Postulates for the Foundation of Logic, The Annals of Mathematics, vol.33, issue.2, pp.346-366, 1932.
DOI : 10.2307/1968337

A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-58, 1940.
DOI : 10.2307/2371199

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

H. B. Curry, Functionality in Combinatory Logic, Proceedings of the National Academy of Sciences, vol.20, issue.11, pp.584-590
DOI : 10.1073/pnas.20.11.584

P. De-groote, A CPS-translation of the ????-calculus, Lecture Notes in Computer Science, vol.787, pp.85-99, 1994.
DOI : 10.1007/BFb0017475

H. Friedman, Classically and Intuitionistically Provably Recursive Functions " Higher Set Theory, pp.21-27, 1978.
DOI : 10.1007/bfb0103100

G. Gentzen, Untersuchungen ???ber das logische Schlie???en. I, Studies in Logic and the Foundations of Mathematics, pp.176-210, 1935.
DOI : 10.1007/BF01201353

P. C. 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éliminationetélimination des coupures dans l'arithmétique d'ordre supérieur " Thèse d'´ etat, 1972.

A. Heyting, Intuitionism : an Introduction, Studies in Logic and the Foundations of Mathematics, 1956.

W. Howard and H. B. , The formulae-as-types notion of construction Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.479-490, 1969.

S. C. Kleene, Introduction to Metamathematics, 1952.

A. N. Kolmogorov, Zur Deutung der intuitionistischen Logik, Mathematische Zeitschrift, vol.35, issue.1, pp.58-65, 1932.
DOI : 10.1007/BF01186549

A. N. Kolmogorov, On the principle of the excluded middle, pp.646-667, 1925.

V. N. Krivtsov, A Negationless Interpretation of Intuitionistic Theories I, Studia Logica, vol.64, issue.3, pp.323-344, 2000.
DOI : 10.1023/A:1005233526469

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

V. F. Mezhlumbekova, Deductive Capabilities of Negationless Intuitionistic Arithmetic, Moscow University Mathematical Bulletin, vol.30, issue.2, 1975.

V. F. Mezhlumbekova, The system of negationless calculus of predicates with meaningfulness operator, Transactions of NAS of Azerbaijan Num. XXIII, vol.4, pp.109-112, 2003.

G. Mints, Notes on Constructive Negation " Synthese, pp.701-717, 2006.
DOI : 10.1007/s11229-004-6294-3

C. R. Murthy, Extracting Constructive Content from Classical Proofs, 1990.

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

G. D. Plotkin, Call-by-name, call-by-value and the ??-calculus, Theoretical Computer Science, vol.1, issue.2, pp.125-159, 1975.
DOI : 10.1016/0304-3975(75)90017-1

H. Poincaré, Dernì eres pensées " Flammarion English translation in " Last thoughts, N. Y, 1913.

D. Prawitz, Natural Deduction, a Proof-theoretical Study, Almquist and Wiksell, 1965.

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

J. Van-heijenhoort, From Frege to Gödel : a source book in mathematical logic, pp.1879-1931, 1967.

P. G. Vredenduin, The Logic of Negationless Mathematics, Compositio Mathematica, vol.11, pp.204-277, 1953.