?. and :. ,

?. , :. , ?. ?-?-q-:-b-|-?;-?-?-?, and ?. ,

?. , :. , ?. ?-|-e-:-b-?-?;-?-?-?, and ?. ,

?. and ?. , If ? ? V : A | ?; ? then: (1) c : (?,a : A, ? ? ? ?; ? ) ? c

?. , :. , ?. ?-?-q-:-b-|-?;-?-?-?, and ?. ,

?. , :. , ?. ?-|-e-:-b-?-?;-?-?-?, and ?. ,

A. , ?. ?-?-u-:-n-|-?;-?-?-?, and ?. ,

?. ?-?,?-:-a,-?-?-;-?-)-?-c-;-?-?-?,-?-?-;-?-?-q-:-b-|-?,?-:-a,-?-?-;-?-?-?-?-q,

D. Ahman, N. Ghani, and G. D. Plotkin, Dependent Types and Fibred Computational Effects, pp.36-54

H. Springer-berlin, , 2016.

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

F. Barbanera and S. Berardi, A symmetric lambda calculus for classical program extraction, Inf. Comput, vol.125, issue.2, pp.103-117, 1996.

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

V. Blot, Hybrid realizability for intuitionistic and classical choice, LICS 2016, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01766881

T. Coquand and C. Paulin, Inductively defined types, pp.50-66, 1990.

P. , L. Curien, and H. Herbelin, The duality of computation, Proceedings of ICFP 2000, vol.35, pp.233-243, 2000.
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, ICFP 2016, 2016.

G. Ferreira and P. Oliva, On various negative translations, Proceedings Third International Workshop on Classical Logic and Computation, CL&C 2010, vol.47, pp.21-33, 2010.

A. Filinski, Representing monads, Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, pp.446-457, 1994.

D. Fridlender and M. Pagano, Pure type systems with explicit substitutions, J. Funct. Program, vol.25, 2015.

H. Friedman, Classically and intuitionistically provably recursive functions, pp.21-27, 1978.

C. Führmann, Direct models for the computational lambda calculus, Electr. Notes Theor. Comput. Sci, vol.20, pp.245-292, 1999.

J. Garrigue, Relaxing the value restriction, Functional and Logic Programming, 7th International Symposium, vol.2998, pp.196-213, 2004.

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.

R. Harper and M. Lillibridge, Polymorphic type assignment and CPS conversion, LISP and Symbolic Computation, vol.6, issue.3, pp.361-379, 1993.

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

H. Herbelin, A constructive proof of dependent choice, compatible with classical logic, Proceedings of the 27th
URL : https://hal.archives-ouvertes.fr/hal-00697240

, Annual IEEE Symposium on Logic in Computer Science, LICS 2012, pp.365-374, 2012.

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

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, vol.42, pp.59-87, 2003.

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

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, vol.9632, pp.476-502, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01107429

R. Lepigre, Semantics and Implementation of an Extension of ML for Proving Programs, 2017.
URL : https://hal.archives-ouvertes.fr/tel-01682908

P. Martin-löf, Constructive mathematics and computer programming, Proc. Of a Discussion Meeting of the Royal Society of London on Mathematical Logic and Programming Languages, pp.167-184, 1985.

A. Miquel, Existential witness extraction in classical realizability and via a negative translation, Logical Methods in Computer Science, vol.7, issue.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, pp.777-803, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01744359

É. Miquey and H. Herbelin, Realizability interpretation and normalization of typed call-by-need ?-calculus with control, Foundations of Software Science and Computation Structures: 21th International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01624839

É. Miquey, A sequent calculus with dependent types for classical arithmetic, Proceedings of the 33nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2018.
URL : https://hal.archives-ouvertes.fr/hal-01703526

G. Munch-maccagnoni, Focalisation and Classical Realisability, Computer Science Logic '09, vol.5771, pp.409-423, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00409793

G. Munch-maccagnoni, Models of a Non-associative Composition, pp.396-410, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00996729

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

C. Paulin-mohring, Extracting F ? '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.

P. , M. Pédrot, and N. Tabareau, An Effectful Way to Eliminate Addiction to Dependence, Logic in Computer Science (LICS), 2017 32nd Annual ACM/IEEE Symposium, vol.12, 2017.

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

M. Vákár, A framework for dependent types and effects, 2015.

M. Vákár, Search of Effectful Dependent Types, 2017.

L. Steffen-van-bakel and . Liquori, Comparing cubes of typed and type assignment systems, Annals of Pure and Applied Logic, vol.86, issue.3, pp.267-303, 1997.

P. Wadler, Call-by-value is dual to call-by-name, Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, pp.189-201, 2003.

A. Wright, Simple imperative polymorphism, LISP and Symbolic Computation, pp.343-356, 1995.