. Proof, We proceed by induction over the typing rules. 9.5, ALGEBRAIC STRUCTURES FOR

. Interestingly, Krivine structure gives rise to a Krivine ordered combinatory algebra, and vice-versa In both cases, the induced triposes (by the AKS and the K OCA) are equivalent. is justiies the claim that the laaer indeed captures the necessary additional structure that allows an OCA induced from an AKS to be a tripos. ese results are a reenement of Proposition 9

. Proof and . See, 13] for the second Without considering in details the proofs of the correspondences between AKS and K OCA or their associated triposes, it is worth noting that when going from a K OCA A to a AKS, both sets ? and ? are deened as A. is means in particular that realizers and their opponents live in the same world, and the orthogonality relation is simply reeected by the order. at is t? ?? if t ? ? , and more generally if X ? P (?), t? ?X if for any x ? X , t ? x. If, as advocated in Section 9.2, we identify a closed formula A with its falsity values A, we recover the intuition that t A is reeected by the ordering t ? A. With these ideas in mind, we are now ready to see the more general notion of implicative algebra, ? ? ) 4. ( S ?U S ) ? ? ? S ?U (S ? ? )

. Proof, e proof is almost the same as for the proof of adequacy for the call-by-name ?µ?µ?µ? ?µ?µ-calculus. We only give some key cases which are peculiar to this seeing. We proceed by induction over the typing derivations

. Proof, Trivial from the deenitions. e ?-reduction is reeected by the preorder

. Proof, Trivial from the deenitions. 1. ? If a a and b b , then ab a b

D. Ahman, N. Ghani, and G. D. Plotkin, Dependent Types and Fibred Computational EEects, pp.36-54
DOI : 10.1007/978-3-662-49630-5_3

S. Amini, Logique classique et calcul, 2015.

Z. Ariola and M. Felleisen, The call-by-need lambda calculus, Journal of Functional Programming, vol.7, issue.3, pp.265-30110, 1993.
DOI : 10.1017/S0956796897002724

Z. M. Ariola, P. Downen, H. Herbelin, K. Nakata, and A. Saurin, Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts, Functional and Logic Programming -11th International Symposium, FLOPS 2012 Proceedings, Lecture Notes in Computer Science, pp.32-4610, 2012.
DOI : 10.1007/978-3-642-29822-6_6
URL : https://hal.archives-ouvertes.fr/hal-00697241

Z. M. Ariola, H. Herbelin, and A. Sabry, A type-theoretic foundation of delimited continuations. Higher-Order and Symbolic Computation, pp.233-273, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00177326

Z. M. Ariola, H. Herbelin, and A. Saurin, Classical Call-by-Need and Duality, Typed Lambda Calculi and Applications -10th International Conference, pp.27-44, 2011.
DOI : 10.1017/S096012950000311X
URL : https://hal.archives-ouvertes.fr/inria-00630156

Z. M. Ariola, J. Maraist, M. Odersky, M. Felleisen, and P. Wadler, A call-by-need lambda calculus, Proceedings of the 22Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '95, pp.233-246, 1995.
DOI : 10.1145/199448.199507

S. Awodey, Category eory. Oxford Logic Guides

S. Banach and A. Tarski, Sur la d??composition des ensembles de points en parties respectivement congruentes, Fundamenta Mathematicae, vol.6, issue.1, pp.244-277, 1924.
DOI : 10.4064/fm-6-1-244-277

H. Barendregt, e Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and e Foundations of Mathematics, 1984.

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

H. P. Barendregt, Lambda calculi with types, Handbook of Logic in Computer Science, vol.2, pp.117-309, 1992.
DOI : 10.1017/cbo9781139032636

G. Barthe, J. Hatclii, and M. H. Sørensen, CPS translations and applications: e cube and beyond. Higher-Order and Symbolic Computation, pp.125-1701010000206149, 1999.

J. L. Bell, Set eory: Boolean-Valued Models and Independence Proofs, 2005.

S. Berardi, M. Bezem, and T. Coquand, Abstract, The Journal of Symbolic Logic, vol.39, issue.02, pp.600-622, 1998.
DOI : 10.1007/BF02007566

U. Berger, A computational interpretation of open induction, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004., pp.14-17, 2004.
DOI : 10.1109/LICS.2004.1319627

V. Blot, Hybrid realizability for intuitionistic and classical choice, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pp.575-584
DOI : 10.1090/pspum/005/0154801
URL : http://dl.acm.org/ft_gateway.cfm?id=2934511&type=pdf

V. Blot, An interpretation of system F through bar recursion, 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2017.
DOI : 10.1109/LICS.2017.8005066

J. Bolyai, e Science Absolute of Space: Independent of the Truth Or Falsity of Euclid's Axiom XI (which Can Never be Decided a Priori)? Neomonic series. Neomon, 1896, 2790.

G. Boole, Investigation of e Laws of ought On Which Are Founded the Mathematical eories of Logic and Probabilities. 1853

]. N. Bourbaki, ´ Eléments de mathématique. ´ eorie des ensembles URL: http://opac.inria.fr/record=b1078957, 1970.

L. Cardelli, S. Martini, J. C. Mitchell, and A. Scedrov, An extension of system F with subtyping, pp.750-770, 1991.

A. Charguéraud, The Locally Nameless Representation, Journal of Automated Reasoning, vol.40, issue.12, pp.363-408, 2012.
DOI : 10.1007/s10817-008-9097-2

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

A. Church, A note on the Entscheidungsproblem, The Journal of Symbolic Logic, vol.166, issue.01, pp.40-4110, 1936.
DOI : 10.1007/BF01475439

A. Church, An Unsolvable Problem of Elementary Number Theory, American Journal of Mathematics, vol.58, issue.2, pp.345-363, 1936.
DOI : 10.2307/2371045

T. Coquand, A semantics of evidence for classical arithmetic, The Journal of Symbolic Logic, vol.54, issue.01, pp.325-33710, 1995.
DOI : 10.1007/BFb0079691

T. Coquand and C. Paulin, Inductively deened types, pp.50-66, 1990.
DOI : 10.1007/3-540-52335-9_47

P. Cousot and R. Cousot, Constructive versions of Tarski's xed point theorems, Paciic Journal of Mathematics, vol.81, issue.1, pp.43-57, 1979.
DOI : 10.2140/pjm.1979.82.43
URL : http://msp.org/pjm/1979/82-1/pjm-v82-n1-p04-s.pdf

T. Crolard, A confluent ??-calculus with a catch/throw mechanism, Journal of Functional Programming, vol.9, issue.6, pp.625-64710, 1999.
DOI : 10.1017/S0956796899003512
URL : https://hal.archives-ouvertes.fr/hal-00094601

P. Curien and H. Herbelin, The duality of computation, Proceedings of ICFP 2000, pp.233-243, 2000.
DOI : 10.1145/357766.351262
URL : https://hal.archives-ouvertes.fr/inria-00156377

H. B. Curry, Functionality in Combinatory Logic, Proceedings of the National Academy of Science, pp.584-590
DOI : 10.1073/pnas.20.11.584
URL : http://doi.org/10.1073/pnas.20.11.584

H. B. Curry, R. Feys35, ]. Dagand, and G. Scherer, Combinatory Logic Normalization by realizability also evaluates URL: https, Vingtsixì emes Journées Francophones des Langages Applicatifs, 1958.

N. Daniels, Thomas Reid's Discovery of a Non-Euclidean Geometry, Philosophy of Science, vol.39, issue.2, pp.219-234, 1972.
DOI : 10.1086/288435

O. Danvy, K. Millikin, J. Munk, and I. Zerny, Defunctionalized Interpreters for Call-by-Need Evaluation, pp.240-256, 2010.
DOI : 10.1007/978-3-642-12251-4_18
URL : http://repository.readscheme.org/ftp/papers/plsemantics/danvy/danvy-al-flops10.pdf

N. De-bruijn, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem, Indagationes Mathematicae (Proceedings), vol.75, issue.5, pp.381-3921385, 1972.
DOI : 10.1016/1385-7258(72)90034-0

P. Downen, L. Maurer, Z. M. Ariola, and S. P. Jones, Sequent calculus as a compiler intermediate language, 2016.
DOI : 10.1145/3022670.2951931

M. H. Escardó and P. Oliva, Abstract, The Journal of Symbolic Logic, vol.344, issue.01
DOI : 10.1016/j.apal.2014.07.003

M. Felleisen, D. P. Friedman, E. E. Kohlbecker, and B. F. Duba, Reasoning with continuations, Proceedings of the Symposium on Logic in Computer Science (LICS '86), pp.131-141, 1986.

G. Ferreira and P. Oliva, On Various Negative Translations, Proceedings ird International Workshop on Classical Logic and Computation, pp.21-33, 2010.
DOI : 10.4204/EPTCS.47.4
URL : http://arxiv.org/pdf/1101.5442.pdf

W. Ferrer-santos, J. Frey, M. Guillermo, O. Malherbe, and A. Miquel, Ordered combinatory algebras and realizability, Mathematical Structures in Computer Science, vol.27, issue.03, pp.428-45810, 2017.
DOI : 10.1111/j.1746-8361.1969.tb01194.x

W. Ferrer-santos, M. Guillermo, and O. Malherbe, Realizability in OCAs and AKSs. ArXiv e-prints, 2015.

A. Filinski, Representing monads, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '94, pp.446-457, 1994.
DOI : 10.1145/174675.178047

M. Fiiing, Intuitionistic Logic, Model eory and Forcing, 1969.

G. Frege, Begriisschrii, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens

. Halle, URL: http://gallica.bnf.fr/ark, 1879.

G. Frege, Posthumous Writings, 1991.

J. Frey, Realizability Toposes from Speciications, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), volume 38 of Leibniz International Proceedings in Informatics (LIPIcs), pp.196-210

J. Frey, Classical Realizability in the CPS Target Language, irty-second Conference on the Mathematical Foundations of Programming Semantics, pp.111-126, 2016.
DOI : 10.1016/j.entcs.2016.09.034

D. Fridlender and M. Pagano, Abstract, Journal of Functional Programming, vol.7, 2015.
DOI : 10.2307/2586554

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

C. Führmann, Direct Models of the Computational Lambda-calculus, Electronic Notes in Theoretical Computer Science, vol.20, issue.04, pp.245-292, 1999.
DOI : 10.1016/S1571-0661(04)80078-1

J. Garrigue, Relaxing the Value Restriction, Functional and Logic Programming, 7th International Symposium, FLOPS 2004 Proceedings, volume 2998 of Lecture Notes in Computer Science, pp.196-213, 2004.
DOI : 10.1007/978-3-540-24754-8_15
URL : http://www.math.nagoya-u.ac.jp/~garrigue/papers/morepoly-long.pdf

G. Gentzen, Untersuchungen ???ber das logische Schlie???en. I, Mathematische Zeitschrift, vol.39, issue.1, pp.176-210, 1935.
DOI : 10.1007/BF01201353

G. Gentzen, Untersuchungen ???ber das logische Schlie???en. II, Mathematische Zeitschrift, vol.39, issue.1, pp.405-431, 1935.
DOI : 10.1007/BF01201363

J. Girard, A new constructive logic: classic logic, Mathematical Structures in Computer Science, vol.7, issue.2, pp.255-29610, 1991.
DOI : 10.1016/0304-3975(87)90045-4

J. Girard, Y. Lafont, and P. Taylor, Proofs and Types [61] K. Gödel. ¨ Uber formal unentscheidbare sätze der principia mathematica und verwandter systeme i, Monatsheee für Mathematik und Physik, pp.173-19810, 1931.

T. G. Griin, A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, POPL '90, pp.47-58, 1990.

M. Guillermo, Jeux de réalisabilité en arithmétique classique, 2008.

M. Guillermo and A. Miquel, Specifying Peirce's law in classical realizability, Mathematical Structures in Computer Science, vol.7, issue.07, pp.1269-1303, 2016.
DOI : 10.1016/S0304-3975(02)00776-4

M. Guillermo and . Miquey, Classical realizability and arithmetical formul??, Mathematical Structures in Computer Science, vol.84, issue.06, pp.1-4010, 2016.
DOI : 10.1007/s001530000057

R. Harper and M. Lillibridge, Polymorphic type assignment and CPS conversion, LISP and Symbolic Computation, vol.89, issue.3, pp.361-379, 1993.
DOI : 10.1007/BF01019463

H. Herbelin, C'est maintenant qu'on calcule: au coeur de la dualité, 2005.

H. Herbelin, On the Degeneracy of ??-Types in Presence of Computational Classical Logic, Typed Lambda Calculi and Applications, 7th International Conference Proceedings, pp.209-220, 2005.
DOI : 10.1007/11417170_16

H. Herbelin, A Constructive Proof of Dependent Choice, Compatible with Classical Logic, 2012 27th Annual IEEE Symposium on Logic in Computer Science, pp.365-374, 2012.
DOI : 10.1109/LICS.2012.47
URL : https://hal.archives-ouvertes.fr/hal-00697240

H. Herbelin and S. Ghilezan, An approach to call-by-name delimited continuations, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.383-394, 2008.
DOI : 10.1145/1328438.1328484
URL : https://hal.archives-ouvertes.fr/inria-00524949

A. Heyting, Mathematische Grundlagenforschung. Intuitionismus. Beweistheorie, 1934.
DOI : 10.1007/978-3-642-65617-0

D. Hilbert, Mathematical problems, Bulletin of the American Mathematical Society, vol.8, issue.10, pp.437-479, 1902.
DOI : 10.1090/S0002-9904-1902-00923-3

D. Hilbert, Königsberg's radio address URL: https://www.maa, 1930.

P. Hofstra, J. Van, and . Oosten, Ordered partial combinatory algebras, Mathematical Proceedings of the Cambridge Philosophical Society, vol.134, issue.3, pp.445-46310, 2003.
DOI : 10.1017/S0305004102006424

W. A. Howard, e formulae-as-types notion of construction, 1969.

J. Hyland, e eeective topos, Studies in Logic and the Foundations of Mathematics, pp.165-21610, 1982.

J. Hyland, P. Johnstone, and A. Piis, Tripos theory, Math. Proc. Camb, pp.205-232, 1980.
DOI : 10.1111/j.1746-8361.1969.tb01194.x

G. Jaber, Krivine Realizability for Compiler Correctness Master's thesis, Ecole des Mines de Nantes URL: https, 2010.

G. Jaber, G. Lewertowski, P. Pédrot, M. Sozeau, and N. Tabareau, e deenitional side of the forcing, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pp.367-376

G. Jaber, N. Tabareau, and M. Sozeau, Extending Type Theory with Forcing, 2012 27th Annual IEEE Symposium on Logic in Computer Science, pp.395-404
DOI : 10.1109/LICS.2012.49
URL : https://hal.archives-ouvertes.fr/hal-00685150

T. J. Jech, e Axiom of Choice. Studies in Logic, 1973.

F. Joachimski and R. Maahes, Short proofs of normalization for the simply-typed ?-calculus, permutative conversions and gödel's t. Archive for Mathematical Logic, pp.59-87, 2003.

P. Johnstone, Sketches of an elephant: a Topos theory compendium. Oxford logic guides, 2002.

D. Kesner, Reasoning About Call-by-need by Means of Types, pp.424-441
DOI : 10.1016/0304-3975(92)90297-S

S. C. Kleene, On the interpretation of intuitionistic number theory, The Journal of Symbolic Logic, vol.3, issue.04, pp.109-124, 1945.
DOI : 10.1007/BF01565439

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

S. A. Kripke, Semantical Considerations on Modal Logic, Acta Philosophica Fennica, vol.16, pp.83-94, 1963.
DOI : 10.1007/978-3-0346-0145-0_16

S. A. Kripke, Semantical analysis of intuitionistic logic i. Studies in Logic and the Foundations of, Mathematics, vol.40, issue.08, pp.92-130, 1965.
DOI : 10.1016/s0049-237x(08)71685-9

J. Krivine, Un algorithme non-typable dans le système f. Comptes rendus de l'Académie des sciences, Mathématiques, vol.1, issue.3045, pp.123-126, 1987.

J. Krivine, Lambda-calculus, types and models, 1993.
URL : https://hal.archives-ouvertes.fr/cel-00574575

J. Krivine, Typed lambda-calculus in classical Zermelo-Fr??nkel set theory, Archive for Mathematical Logic, vol.40, issue.3, pp.189-205, 2001.
DOI : 10.1007/s001530000057

J. Krivine, Dependent choice, ???quote??? and the clock, Theoretical Computer Science, vol.308, issue.1-3, pp.259-276, 2003.
DOI : 10.1016/S0304-3975(02)00776-4
URL : https://hal.archives-ouvertes.fr/hal-00154478

J. Krivine, A call-by-name lambda-calculus machine, Higher Order and Symbolic Computation, 2004.
DOI : 10.1093/comjnl/6.4.308
URL : https://hal.archives-ouvertes.fr/hal-00154508

J. Krivine, A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation, pp.199-207, 2007.
DOI : 10.1007/s10990-007-9018-9
URL : https://hal.archives-ouvertes.fr/hal-00154508

J. Krivine, Realizability in classical logic In interactive models of computation and program behaviour, Panoramas et synthèses, vol.27, 2009.

J. Krivine, Realizability algebras: a program to well order R, Logical Methods in Computer Science, vol.40, issue.3, 2011.
DOI : 10.1007/s001530000057
URL : https://hal.archives-ouvertes.fr/hal-00483232

J. Krivine, Realizability algebras II : new models of ZF + DC, Logical Methods in Computer Science, vol.8, issue.1, p.10, 2012.
DOI : 10.1007/s001530000057
URL : https://hal.archives-ouvertes.fr/hal-00497587

J. Krivine, elques propriétés des modèles de réalisabilité de ZF, Feb, 2014.

J. Krivine, On the Structure of Classical Realizability Models of ZF, 20th International Conference on Types for Proofs and Programs of Leibniz International Proceedings in Informatics (LIPIcs), pp.146-161, 2014.

J. Krivine, Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis, 25th EACSL Annual Conference on Computer Science Logic of Leibniz International Proceedings in Informatics (LIPIcs), pp.1-25, 2016.

Y. Lafont, B. Reus, and T. Streicher, Continuations semantics or expressing implication by negation, 1993.

F. Lang, Explaining the lazy krivine machine using explicit substitution and addresses. Higher- Order and Symbolic Computation, pp.257-270, 2007.
DOI : 10.1007/s10990-007-9013-1
URL : https://hal.archives-ouvertes.fr/inria-00198756

F. Lawvere, Adjointness in Foundations, dialectica, vol.71, issue.3-4, pp.281-296, 1969.
DOI : 10.1073/pnas.50.5.869
URL : http://www.tac.mta.ca/tac/reprints/articles/16/tr16a.pdf

G. W. Leibniz, Die philosophischen Schriien URL: https://archive, 1890.

R. Lepigre, A Classical Realizability Model for a Semantical Value Restriction, Programming Languages and Systems -25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on eory and Practice of Sooware Proceedings, volume 9632 of Lecture Notes in Computer Science, pp.476-502, 2016.
DOI : 10.1145/292540.292560
URL : https://hal.archives-ouvertes.fr/hal-01107429

P. B. Levy, Call-By-Push-Value: A Functional/Imperative Synthesis, volume 2 of Semantics Structures in Computation, 2004.
DOI : 10.1007/978-94-007-0954-6

N. Lobatchevsky, Géométrie imaginaire, Journal für die reine und angewandte Mathematik, pp.295-320, 1837.

S. Maclane and I. Moerdijk, Sheaves in Geometry and Logic, 1992.

J. Maraist, M. Odersky, and P. Wadler, The call-by-need lambda calculus, Journal of Functional Programming, vol.8, issue.3, pp.275-317, 1994.
DOI : 10.1017/S0956796898003037

J. Maraist, M. Odersky, and P. Wadler, The call-by-need lambda calculus, Journal of Functional Programming, vol.8, issue.3, pp.275-31710, 1998.
DOI : 10.1017/S0956796898003037

P. Martin-löf, Constructive Mathematics and Computer Programming, Proc. Of a Discussion, pp.167-184, 1985.
DOI : 10.1016/S0049-237X(09)70189-2

P. Martin-löf, An intuitionistic theory of types In twenty--ve years of constructive type theory. Oxford Logic Guides, pp.127-172, 1998.

I. Moerdijk and J. Van-oosten, Topos theory, 2007.

E. Moggi, Computational lambda-calculus and monads, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, 1988.
DOI : 10.1109/LICS.1989.39155

G. Muller, e axiom of choice is wrong URL: https://cornellmath.wordpress.com, 2007.

G. Munch-maccagnoni, Focalisation and Classical Realisability, Computer Science Logic '09, pp.409-423
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00409793

G. Munch-maccagnoni, Models of a Non-associative Composition, pp.396-410, 2014.
DOI : 10.1007/978-3-642-54830-7_26
URL : https://hal.archives-ouvertes.fr/hal-00996729

C. Okasaki, P. Lee, and D. Tarditi, Call-by-need and continuation-passing style, Lisp and Symbolic Computation, pp.57-82, 1994.
DOI : 10.1007/BF01019945
URL : http://www-cgi.cs.cmu.edu/afs/cs.cmu.edu/project/fox/mosaic/papers/petel-lazy-p.ps

P. Oliva and T. Streicher, On Krivine's realizability interpretation of classical second-order arithmetic, Fundam. Inform, vol.84, issue.2, pp.207-220, 2008.

M. Parigot, Free deduction: An analysis of ???Computations??? in classical logic, Proceedings of LPAR, pp.361-380, 1991.
DOI : 10.1007/3-540-55460-2_27

M. Parigot, Abstract, The Journal of Symbolic Logic, vol.50, issue.04, pp.1461-1479, 1997.
DOI : 10.1145/322358.322370

C. Paulin-mohring, Extracting ??'s programs from proofs in the calculus of constructions, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '89, pp.89-104, 1989.
DOI : 10.1145/75277.75285

P. Pédrot, . Materialist-dialectica, P. Eses, and . Diderot, URL: https://hal. archives-ouvertes, p.1247085, 2015.

P. Pédrot and A. Saurin, Classical By-Need, pp.616-643, 2016.
DOI : 10.1017/S0956796898003141

A. Piis, e eory of Triposes, 1981.

A. M. Piis, Tripos theory in retrospect, Mathematical Structures in Computer Science, vol.12, issue.3, pp.265-27910, 2002.

G. Plotkin, LCF considered as a programming language, Theoretical Computer Science, vol.5, issue.3, pp.223-25510, 1977.
DOI : 10.1016/0304-3975(77)90044-5
URL : https://doi.org/10.1016/0304-3975(77)90044-5

G. Plotkin and J. Power, Notions of Computation Determine Monads, pp.342-356, 2002.
DOI : 10.1007/3-540-45931-6_24

G. D. Plotkin, Call-by-name, call-by-value and the lambda-calculus. eor, Comput. Sci, vol.1, issue.275, pp.125-15910, 1975.
DOI : 10.1016/0304-3975(75)90017-1
URL : https://doi.org/10.1016/0304-3975(75)90017-1

E. Polonovski, Strong Normalization of $\overline{\lambda}\mu\widetilde{\mu}$ -Calculus with Explicit Substitutions, FOSSACS, pp.423-437, 2004.
DOI : 10.1007/978-3-540-24727-2_30

P. Pédrot and N. Tabareau, An eeectful way to eliminate addiction to dependence, Proc. Of LICS2017, 2017.

T. Reid, Géométrie des visibles URL: https, OEuvrescompì etes, pp.186-203, 1828.

L. Rieg, Extracting Herbrand trees in classical realizability using forcing, Computer Science Logic 2013 of Leibniz International Proceedings in Informatics (LIPIcs), pp.597-614, 2013.
URL : https://hal.archives-ouvertes.fr/ensl-00814278

L. Rieg, On Forcing and Classical Realizability. eses, Ecole normale supérieure de lyon -ENS LYON URL: https, 2014.
URL : https://hal.archives-ouvertes.fr/tel-01061442

]. B. Riemann, ¨ Uber die hypothesen, welche der geometrie zu grunde liegen
DOI : 10.1007/978-3-7091-3071-1_3

B. Russell, Introduction to Mathematical Philosophy, 1919.

F. Ruyer, Proofs, Types and Subtypes URL: https: //tel.archives-ouvertes, p.140046, 2006.

A. Sabry and M. Felleisen, Reasoning about programs in continuation-passing style, Lisp and Symbolic Computation, vol.6, pp.3-4289, 1993.
DOI : 10.1007/bf01019462

S. G. Simpson, Subsystems of Second Order Arithmetic. Perspectives in Logic, pp.10-1017, 2009.

C. Spector, Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics, Recursive function theory: Proceedings of symposia in pure mathematics, pp.1-27, 1962.
DOI : 10.1090/pspum/005/0154801

T. Streicher, Krivine's classical realisability from a categorical perspective, Mathematical Structures in Computer Science, vol.27, issue.06, pp.1234-125610, 2013.
DOI : 10.1016/S0304-3975(02)00776-4

G. J. Sussman, G. L. Steele, and J. , An interpreter for extended lambda calculus, Massachusees Institute of Technology, 1975.

A. Tarski, e concept of truth in the languages of the deductive sciences, pp.152-278, 1953.

A. M. Turing, On computable numbers, with an application to the entscheidungsproblem, Proceedings of the London Mathematical Society, issue.1, pp.2-42230, 1937.

A. M. Turing, On computable numbers, with an application to the entscheidungsproblem. a correction, Proceedings of the London Mathematical Society, pp.2-43544, 1938.

S. Van-bakel, L. Liquori, S. R. Della-rocca, and P. Urzyczyn, Comparing cubes of typed and type assignment systems, Annals of Pure and Applied Logic, vol.86, issue.3, pp.267-30310, 1997.
DOI : 10.1016/S0168-0072(96)00036-X
URL : https://hal.archives-ouvertes.fr/hal-01154638

D. Van-dalen, Intuitionistic logic, pp.224-257, 2001.

J. Van-oosten, Realizability: a historical essay, Mathematical Structures in Computer Science, vol.12, issue.03, pp.239-26310, 2002.
DOI : 10.1017/S0960129502003626

J. Van-oosten, Studies in logic and the foundations of mathematics In Realizability: An Introduction to its Categorical Side, of Studies in Logic and the Foundations of Mathematics, pp.10-1016, 2008.

A. Wright, Simple imperative polymorphism, LISP and Symbolic Computation, pp.343-356, 1995.
DOI : 10.1007/BF01018828
URL : http://www.dcs.ed.ac.uk/home/dts/aps/papers/wright.ps.gz

E. Zermelo, Beweis, dass jede menge wohlgeordnet werden kann. (aus einem an herrn hilbert gerichteten briefe) Mathematische Annalen, pp.514-516, 1904.
DOI : 10.1007/bf01445300