Z. Ariola and M. Felleisen, The call-by-need lambda calculus, Journal of Functional Programming, vol.7, issue.3, pp.265-301, 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, Proceedings of FLOPS'12. Proceedings, LNCS, pp.32-46, 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 continuations and prompts, Proceedings of ICFP'04, pp.40-53, 2004.

Z. M. Ariola, H. Herbelin, and A. Saurin, Classical Call-by-Need and Duality, Proceedings of TLCA 2011, pp.27-44, 2011.
DOI : 10.1017/S096012950000311X

URL : https://hal.archives-ouvertes.fr/inria-00630156

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

T. Crolard, A confluent ??-calculus with a catch/throw mechanism, Journal of Functional Programming, vol.9, issue.6, pp.625-647, 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

P. Dagand and G. Scherer, Normalization by realizability also evaluates, Proceedings of JFLA'15, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01099138

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.
DOI : 10.1016/1385-7258(72)90034-0

M. Felleisen, D. P. Friedman, E. E. Kohlbecker, and B. F. Duba, Reasoning with continuations, Proceedings of LICS'86, pp.131-141, 1986.

J. Girard, Y. Lafont, and P. Taylor, Proofs and Types, 1989.

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

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

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

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

J. Krivine, Lambda-calculus, types and models. Ellis Horwood series in computers and their applications, 1993.
URL : https://hal.archives-ouvertes.fr/cel-00574575

J. Krivine, Realizability in classical logic In interactive models of computation and program behaviour, 2009.

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

R. Lepigre, A classical realizability model for a semantical value restriction Held as Part of the European Joint Conferences on Theory and Practice of Software, Programming Languages and Systems -25th European Symposium on Programming Proceedings, volume 9632 of Lecture Notes in Computer Science, pp.476-502, 2016.

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

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.2787

G. Munch-maccagnoni, Focalisation and Classical Realisability, Computer Science Logic '09, pp.409-423, 2009.
DOI : 10.1016/0304-3975(87)90045-4

URL : https://hal.archives-ouvertes.fr/inria-00409793

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://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.43.7282

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

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

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

URL : http://doi.org/10.1016/0304-3975(75)90017-1

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

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.122.1481