D. Ahman, N. Ghani, and G. D. Plotkin, Dependent Types and Fibred Computational Effects, pp.36-54
DOI : 10.1007/978-3-662-46678-0_7

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

F. Barbanera and S. Berardi, A Symmetric Lambda Calculus for Classical Program Extraction, Information and Computation, vol.125, issue.2, pp.103-117, 1996.
DOI : 10.1006/inco.1996.0025
URL : http://doi.org/10.1006/inco.1996.0025

G. Barthe, J. Hatcliff, M. Heine, and B. Sørensen, CPS translations and applications: The cube and beyond. Higher-Order and Symbolic Computation, pp.125-170, 1999.

V. Blot, Hybrid realizability for intuitionistic and classical choice, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, 2016.
DOI : 10.1145/2933575.2934511

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

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. Downen, L. Maurer, Z. M. Ariola, and S. Jones, Sequent calculus as a compiler intermediate language, 2016.
DOI : 10.1145/3022670.2951931

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

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

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, 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 Proceedings, volume 2998 of Lecture Notes in Computer Science, pp.196-213, 2004.
DOI : 10.1007/978-3-540-24754-8_15
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.100.4779

T. G. Griffin, 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.
DOI : 10.1145/96709.96714

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

H. Herbelin, On the degeneracy of sigma-types in presence of computational classical logic, Proceedings of TLCA 2005, pp.209-220, 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

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/1328897.1328484
URL : https://hal.archives-ouvertes.fr/inria-00524949

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

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

J. Krivine, Realizability in classical logic In interactive models of computation and program behaviour. Panoramas et synthèses, pp.197-229, 2009.

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.

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

A. Miquel, Existential witness extraction in classical realizability and via a negative translation, Logical Methods in Computer Science, vol.7, issue.2, 2011.
DOI : 10.2168/LMCS-7(2:2)2011
URL : https://hal.archives-ouvertes.fr/hal-00800560

É. Miquey, A classical sequent calculus with dependent types Held as Part of the European Joint Conferences on Theory and Practice of Software, Programming Languages and Systems: 26th European Symposium on Programming Proceedings, pp.777-803, 2017.

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

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

E. Polonovski, Strong normalization of lambda-bar-mu-mu-tilde-calculus with explicit substitutions, FOSSACS, volume 2987 of Lecture Notes in Computer Science, pp.423-437, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00004321

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

M. Vákár, A framework for dependent types and effects. CoRR, abs, 1512.

A. Wright, Simple imperative polymorphism, LISP and Symbolic Computation, pp.343-356, 1995.
DOI : 10.1007/BF01018828
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.5096