B. Accattoli, P. Barenbaum, and D. Mazza, Distilling abstract machines, Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, pp.363-376, 2014.

B. Accattoli and B. Barras, Environments and the Complexity of Abstract Machines, The 19th International Symposium on Principles and Practice of Declarative Programming, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01675358

,

A. W. Appel, Compiling with Continuations, 1992.

Z. Ariola and M. Felleisen, The call-by-need lambda calculus, J. Funct. Program, vol.7, issue.3, pp.265-301, 1993.

Z. M. Ariola, P. Downen, H. Herbelin, K. Nakata, and A. Saurin, Classical call-byneed sequent calculi: The unity of semantic artifacts, Functional and Logic Programming-11th International Symposium, FLOPS 2012, pp.32-46, 2012.

T. Balabonski, P. Barenbaum, E. Bonelli, and D. Kesner, Foundations of strong call by need, Proc. ACM Program. Lang. 1(ICFP), vol.20, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01766206

,

V. Blot, An interpretation of system f through bar recursion, 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp.1-12, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01766883

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-392, 1972.

,

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

P. Crégut, Strongly reducing variants of the krivine abstract machine, Higher-Order and Symbolic Computation, vol.20, issue.3, pp.209-230, 2007.

,

P. L. Curien and H. Herbelin, The duality of computation, Proceedings of ICFP, 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 Callby-Need Evaluation, pp.240-256, 2010.

M. Felleisen and D. P. Friedman, Control operators, the SECD-machine, and the lambda-calculus, 3rd Working Conference on the Formal Description of Programming Concepts, 1986.

M. Felleisen and A. Sabry, Continuations in programming practice: Introduction and survey, 1999.

M. Felleisen, D. P. Friedman, E. Kohlbecker, and B. Duba, A syntactic theory of sequential control, Theor. Comput. Sci, vol.52, issue.3, pp.90109-90114, 1987.

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

H. Herbelin, A constructive proof of dependent choice, compatible with classical logic, Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, pp.365-374, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00697240

G. Jaber, G. Lewertowski, P. M. Pédrot, M. Sozeau, and N. Tabareau, The definitional side of the forcing, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pp.367-376, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01319066

G. Jaber, N. Tabareau, and M. Sozeau, Extending type theory with forcing, Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science, pp.395-404, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00685150

D. Kesner, Reasoning About Call-by-need by Means of Types, pp.424-441, 2016.

S. A. Kripke, Semantical considerations on modal logic, Acta Philosophica Fennica, vol.16, pp.83-94, 1963.

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

J. L. Krivine, Realizability algebras: a program to well order r, Logical Methods in Computer Science, vol.7, issue.3, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00483232

P. J. Landin, The mechanical evaluation of expressions, The Computer Journal, vol.6, issue.4, pp.308-320, 1964.

F. Lang, Explaining the lazy krivine machine using explicit substitution and addresses, Higher-Order and Symbolic Computation, vol.20, issue.3, pp.257-270, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00198756

X. Leroy, The ZINC experiment: an economical implementation of the ML language, Technical report, vol.117, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00070049

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

J. Maraist, M. Odersky, and P. Wadler, The call-by-need lambda calculus, J. Funct. Program, vol.8, issue.3, pp.275-317, 1998.

P. A. Mellì-es, Local States in String Diagrams, pp.334-348, 2014.

A. Miquel, Forcing as a program transformation, LICS. pp, pp.197-206, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00800558

E. Miquey, A sequent calculus with dependent types for classical arithmetic, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pp.720-729, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01703526

H. Herbelin, ´. E. Miquey, ´. E. Miquey, and H. Herbelin, Realizability Interpretation and Normalization of Typed Call-by-Need ?-calculus With Control, FOSSACS 18-21st International Conference on Foundations of Software Science and Computation Structures. Thessalonique, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01624839

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

C. Murthy, Extracting constructive content from classical proofs, 1990.

C. Okasaki, P. Lee, and D. Tarditi, Call-by-need and continuationpassing style, Lisp and Symbolic Computation, vol.7, pp.57-82, 1994.

,

M. Parigot, Proofs of strong normalisation for second order classical natural deduction, J. Symb. Log, vol.62, issue.4, pp.1461-1479, 1997.

G. Plotkin and J. Power, Notions of Computation Determine Monads, pp.342-356, 2002.

G. D. Plotkin, Call-by-name, call-by-value and the lambda-calculus, Theor. Comput. Sci, vol.1, issue.2, pp.90017-90018, 1975.

P. Sestoft, Deriving a lazy abstract machine, J. Funct. Program, vol.7, issue.3, pp.231-264, 1997.

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

. If-?-v-v-:-t-then-?-v-v,

. If-?-e-e-:-t-?-?-then-?-e-e-:-t-?-?,

, The proof is very similar (and easier) than the proof in the call-by-need case, by induction on typing derivations, If ? ? ? then ? ? ? : ? Proof