. C. We, . Sn, A. Reducible-of-type, and . Sn, If V is some variable x then redexes of J c [E[xV ]] are either in J c [E] or in V which are SN by Lemma 2. If V is some ?x.M then, by definition of its reducibility, V V is reducible

. C. We and . Sn, By the previous item, J c [E[V ]] is a reducible context of type A. Hence

Z. M. Ariola and H. Herbelin, Minimal Classical Logic and Control Operators, Thirtieth International Colloquium on Automata, Languages and Programming , ICALP'03, pp.871-885, 2003.
DOI : 10.1007/3-540-45061-0_68
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.57.6941

Z. M. Ariola and H. Herbelin, Control reduction theories: the benefit of structural substitution, Journal of Functional Programming, vol.18, issue.03, 2007.
DOI : 10.1145/317636.317779
URL : https://hal.archives-ouvertes.fr/inria-00177320

Z. M. Ariola, H. Herbelin, and A. Sabry, A Type-Theoretic Foundation of Continuations and Prompts, ACM SIGPLAN International Conference on Functional Programming, pp.40-53, 2004.

K. Baba, S. Hirokawa, and K. Etsu-fujita, Parallel Reduction in Type Free ????-Calculus, Electronic Notes in Theoretical Computer Science, vol.42, pp.52-66, 2001.
DOI : 10.1016/S1571-0661(04)80878-8

F. Barbanera and S. Berardi, Extracting constructive content from classical logic via control-like reductions, Proceedings 1st Intl. Conf. on Typed Lambda Calculi and Applications, TLCA'93, pp.16-18, 1993.
DOI : 10.1007/BFb0037097
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.120.386

T. Crolard, Subtractive logic, Theoretical Computer Science, vol.254, issue.1-2, pp.151-185, 2001.
DOI : 10.1016/S0304-3975(99)00124-3
URL : https://hal.archives-ouvertes.fr/hal-00094589

T. Crolard, A Formulae-as-Types Interpretation of Subtractive Logic, Journal of Logic and Computation (Special issue on Modalities in Constructive Logics and Type Theories), pp.529-570, 2004.
DOI : 10.1093/logcom/14.4.529
URL : https://hal.archives-ouvertes.fr/hal-00094584

P. Curien and H. Herbelin, The duality of computation, ACM SIG- PLAN International Conference on Functional Programming, pp.233-243, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00156377

O. Danvy and A. Filinski, A Functional Abstraction of Typed Contexts, 1989.

O. Danvy and A. Filinski, Abstracting control, Proceedings of the 1990 ACM conference on LISP and functional programming , LFP '90, pp.151-160, 1990.
DOI : 10.1145/91556.91622

R. David and W. Py, Abstract, The Journal of Symbolic Logic, vol.121, issue.01, pp.407-413, 2001.
DOI : 10.2307/2694930

P. De-groote, On the Relation between the lambda-mu Calculus and the Syntactic Theory of Sequential Control, Logic Programming and Automated Reasoning, Proc. of the 5th International Conference, LPAR'94, pp.31-43, 1994.

R. K. Dybvig, S. Peyton-jones, and A. Sabry, A Monadic Framework for Subcontinuations, 2004.

M. Felleisen, The theory and practice of first-class prompts, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '88, pp.180-190, 1988.
DOI : 10.1145/73560.73576

M. Felleisen, On the Expressive Power of Programming Languages, ESOP '90 3rd European Symposium on Programming, pp.134-151, 1990.

M. Felleisen, D. Friedman, and E. Kohlbecker, A syntactic theory of sequential control, Theoretical Computer Science, vol.52, issue.3, pp.205-237, 1987.
DOI : 10.1016/0304-3975(87)90109-5

M. Felleisen and R. Hieb, The revised report on the syntactic theories of sequential control and state, Theoretical Computer Science, vol.103, issue.2, pp.235-271, 1992.
DOI : 10.1016/0304-3975(92)90014-7

M. Felleisen, M. Wand, D. P. Friedman, and B. F. Duba, Abstract continuations: a mathematical semantics for handling full jumps, Proceedings of the 1988 ACM conference on LISP and functional programming , LFP '88, pp.52-62, 1988.
DOI : 10.1145/62678.62684

A. Filinski, Declarative Continuations: an Investigation of Duality in Programming Language Semantics'. In: Category Theory and Computer Science, Proceedings, pp.224-249, 1989.

A. Filinski, Representing monads, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '94, pp.17-21, 1994.
DOI : 10.1145/174675.178047

A. Filinski, Representing layered monads, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, pp.175-188, 1999.
DOI : 10.1145/292540.292557
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.2016

M. J. Fischer, Lambda-calculus schemata) of SIGPLAN Notices, Proc. ACM Conference on Proving Assertions About Programs, pp.104-109, 1972.

M. J. Fischer, Lambda-calculus schemata, html> Earlier version available in the proceedings of an ACM Conference on Proving Assertions about Programs, SIGPLAN Notices, pp.259-288, 1972.
DOI : 10.1007/BF01019461

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.17-19, 1990.
DOI : 10.1145/96709.96714

C. A. Gunter, D. Rémy, and J. G. Riecke, A generalization of exceptions and control in ML-like languages, Proceedings of the seventh international conference on Functional programming languages and computer architecture , FPCA '95, 1995.
DOI : 10.1145/224164.224173

J. Guzmán and A. Suárez, An Extended Type System for Exceptions, Record of the fifth ACM SIGPLAN workshop on ML and its Applications. Also appeared as Research Report 2265, 1994.

C. Haynes, Logic continuations, Logic Continuations'. In: Proceedings of the Third International Conference on Logic Programming, pp.671-685, 1986.
DOI : 10.1007/3-540-16492-8_117

C. T. Haynes, D. Friedman, and M. Wand, Obtaining coroutines with continuations, Computer Languages, vol.11, issue.3-4, pp.143-153, 1986.
DOI : 10.1016/0096-0551(86)90007-X

H. Herbelin, Explicit Substitutions and Reducibility, Journal of Logic and Computation, vol.11, issue.3, pp.431-451, 2001.
DOI : 10.1093/logcom/11.3.431

R. Hieb and R. K. Dybvig, ) of SIGPLAN NOTICES, Continuations and Concurrency'. In: PPoPP '90, Symposium on Principles and Practice of Parallel Programming, pp.128-136, 1990.

M. Hofmann, Sound and complete axiomatisations of call-by-value control operators, Mathematical Structures in Computer Science, vol.10, issue.04, pp.461-482, 1995.
DOI : 10.1007/BF01019462

W. Howard, The formulae-as-types notion of construction, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, pp.479-490, 1980.

Y. Kameyama, A Type-Theoretic Study on Partial Continuations, pp.489-504, 2000.
DOI : 10.1007/3-540-44929-9_34

Y. Kameyama, Towards Logical Understanding of Delimited Continuations, Proceedings of the Third ACM SIGPLAN Workshop on Continuations (CW'01), 2001.

Y. Kameyama and M. Hasegawa, A Sound and Complete Axiomatization of Delimited Continuations, Proc. of 8th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP'03 SIGPLAN Notices, pp.25-29, 2003.

M. Lillibridge, Unchecked Exceptions Can be Strictly More Powerful Than Call, Higher-Order and Symbolic Computation, pp.75-104, 1999.

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

L. Moreau, A Syntactic Theory of Dynamic Binding'. Higher Order Symbol, Comput, vol.11, issue.3, pp.233-279, 1998.

L. Moreau and C. Queinnec, Partial continuations as the difference of continuations a duumvirate of control operators, International Conference on Programming Language Implementation and Logic Programming (PLILP'94), 1994.
DOI : 10.1007/3-540-58402-1_14

C. Murthy, Control Operators, Hierarchies, and Pseudo-Classical Type Systems: A-Translation at Work', ACM workshop on Continuations, pp.49-71, 1992.

C. L. Ong and C. A. Stewart, A Curry-Howard foundation for functional computation with control, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.15-17, 1997.
DOI : 10.1145/263699.263722

M. Parigot, Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction, Logic Programming and Automated Reasoning: International Conference LPAR '92 Proceedings, pp.190-201, 1992.

C. Rauszer, Semi-boolean algebras and their application to intuitionistic logic with dual connectives, Fundamenta Mathematicae, vol.83, pp.219-249, 1974.

J. G. Riecke and H. Thielecke, Typed Exceptions and Continuations Cannot Macro-Express Each Other, Proceedings of the 26th International Colloquium on Automata, Languages and Programming (ICALP), pp.635-644, 1999.
DOI : 10.1007/3-540-48523-6_60
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.7950

C. Shan, Shift to Control, Proceedings of the 5th workshop on Scheme and Functional Programming, pp.99-107, 2004.

D. Sitaram and M. Felleisen, Control delimiters and their hierarchies, Lisp and Symbolic Computation, pp.67-99, 1990.
DOI : 10.1007/BF01806126

D. Sitaram and M. Felleisen, Reasoning with continuations II: full abstraction for models of control, Proceedings of the 1990 ACM conference on LISP and functional programming , LFP '90, pp.161-175, 1990.
DOI : 10.1145/91556.91626

H. Thielecke, On Exceptions Versus Continuations in the Presence of State, Proceedings of the ninth European Symposium On Programming (ESOP), pp.397-411, 2000.
DOI : 10.1007/3-540-46425-5_26

H. Thielecke, Contrasting Exceptions and Continuations'. Available from http, 2001.

H. Thielecke, Comparing Control Constructs by Double-barrelled CPS Transforms, Higher-order and Symbolic Computation, pp.119-136, 2002.
DOI : 10.1016/S1571-0661(04)80974-5
URL : http://doi.org/10.1016/s1571-0661(04)80974-5

P. Wadler, Monads and composable continuations, Lisp and Symbolic Computation, pp.39-56, 1994.
DOI : 10.1007/BF01019944

M. Wand, Continuation-based multiprocessing, Proceedings of the 1980 ACM conference on LISP and functional programming , LFP '80, pp.285-299, 1999.
DOI : 10.1145/800087.802786
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.44.5351