Z. M. Ariola, P. Downen, H. Herbelin, K. Nakata, and A. Saurin, Classical call-byneed sequent calculi: The unity of semantic artifacts, FLOPS 2012, Proceedings, pp.32-46, 2012.

S. Berardi, M. Bezem, and T. Coquand, On the computational content of the axiom of choice, J. Symb. Log, vol.63, issue.2, pp.600-622, 1998.

U. Berger, A computational interpretation of open induction, LICS 2004, Proceedings, p.326, 2004.

V. Blot, An interpretation of system F through bar recursion, LICS 2017, Proceedings, pp.1-12, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01766883

L. Cohen, V. Rahli, M. Bickford, and R. L. Constable, Computability beyond church-turing using choice sequences, LICS 2018, Proceedings, 2018.

P. Cousot and R. Cousot, Constructive versions of Tarski's xed point theorems, Pacic 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

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

O. Danvy, K. Millikin, J. Munk, and I. Zerny, Defunctionalized interpreters for call-by-need evaluation, FLOPS 2010, Proceedings, pp.240-256, 2010.
DOI : 10.1007/978-3-642-12251-4_18

P. Downen, L. Maurer, Z. M. Ariola, and S. P. Jones, Sequent calculus as a compiler intermediate language, ICFP 2016, Proceedings, 2016.
DOI : 10.1145/2951913.2951931
URL : http://dl.acm.org/ft_gateway.cfm?id=2951931&type=pdf

M. H. Escardó and P. Oliva, Bar recursion and products of selection functions. CoRR, abs/1407, vol.7046, 2014.

H. Herbelin, On the degeneracy of sigma-types in presence of computational classical logic, TLCA 2005, Proceedings, vol.3461, pp.209-220, 2005.

H. Herbelin, A constructive proof of dependent choice, compatible with classical logic, LICS 2012, Proceedings, pp.365-374, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00697240

A. Kolmogoro, Zur deutung der intuitionistischen logik, Mathematische Zeitschrift, vol.35, issue.1, pp.58-65, 1932.

J. Krivine, Dependent choice, 'quote' and the clock, Th. Comp. Sc, vol.308, pp.259-276, 2003.
DOI : 10.1016/s0304-3975(02)00776-4
URL : https://hal.archives-ouvertes.fr/hal-00154478

J. Krivine, Realizability in classical logic, interactive models of computation and program behaviour. Panoramas et synthèses, vol.27, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00154500

J. Krivine, Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis, CSL 2016, Proceedings, volume 62 of LIPIcs, vol.25, pp.1-25, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01090769

R. Lepigre, A classical realizability model for a semantical value restriction, Proceedings, vol.9632, pp.476-502, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01107429

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

É. Miquey, Classical realizability and side-eects. Theses, Univ.é Paris Diderot

. Univ and . De-la-república, , 2017.

É. Miquey, A classical sequent calculus with dependent types, ESOP 2017, Proceedings, pp.777-803, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01519929

É. Miquey and H. Herbelin, Realizability interpretation and normalization of typed call-by-need ?-calculus with control, FoSSaCS, Proceedings, pp.276-292, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01624839

G. Munch-maccagnoni, Syntax and Models of a non-Associative Composition of Programs and Proofs, 2013.
URL : https://hal.archives-ouvertes.fr/tel-00918642

G. Munch-maccagnoni and G. Scherer, Polarised Intermediate Representation of Lambda Calculus with Sums, LICS 2015, Proceedings, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01160579

S. G. Simpson, Subsystems of Second Order Arithmetic. Perspectives in Logic, 2009.

C. Spector, Provably recursive functionals of analysis: A consistency proof of analysis by an extension of principles in current intuitionistic mathematics, Recursive function theory: Proceedings of symposia in pure mathematics, vol.5, pp.1-27, 1962.

, The same applies with |A ? | p , A ? e , etc

. Proof, By induction on the structure of A ? and the dierent levels of interpretation. The dierent base cases (p ? A ? , t ? T , t = u) are direct since their components along ? are dened modulo ? ? , the other cases are trivial inductions. We can now give the complete proof of adequacy of the typing rules with respect to the realizability interpretation

, ? ? a pole, ? a valuation and ? a store such that (? , ?) ?; ? , then the following hold: 1. If is a strong value such that ? ? ? : A or ? ? d : A; ? , then ( |? ) ? ? |A ? | V. 2. If f is a forcing context such that ? ? ? f : A ? ? or ? ?, The typing rules are adequate with respect to the realizability interpretation. In other words, if ? is a typing context

, If V is a weak value such that ? ? ? V : A or ? ? d V : A; ? , then (V |? ) ? ? |A ? | V

, If c? ? is a closure such that ? ? ? c? ? or ? ? d c? ? ; ? , then (c?? ? ) ? ? ? ?

, The proof is done by induction on the typing derivation such as given in the system extended with the small-step reduction s. Most of the cases correspond to the proof of adequacy for the interpretation of the ? [l? ?]-calculus, so that we only give the most interesting cases