M. Zena, H. Ariola, and . Herbelin, Control reduction theories: the benefit of structural substitution, J. Funct. Program, 2007.

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

K. Baba, S. Hirokawa, and K. 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

M. Biernacka, D. Biernacki, and O. Danvy, An Operational Foundation for Delimited Continuations, BRICS Report Series, vol.10, issue.41, 2003.
DOI : 10.7146/brics.v10i41.21809

D. Biernacki and O. Danvy, On the dynamic extent of delimited continuations, 2005.

P. Curien and H. Herbelin, The duality of computation, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, pp.233-243, 2000.
DOI : 10.1145/357766.351262
URL : https://hal.archives-ouvertes.fr/inria-00156377

V. Danos, H. Herbelin, and L. Regnier, Game semantics and abstract machines, Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, pp.394-405, 1996.
DOI : 10.1109/LICS.1996.561456

O. Danvy and A. Filinski, A functional abstraction of typed contexts, 1989.

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

P. A. De-groote, . Cps-94, and U. K. Edinburgh, A CPS-translation of the ????-calculus, Proceedings of the Colloquium on Trees in Algebra and Programming, pp.85-99, 1994.
DOI : 10.1007/BFb0017475

K. Do?en and Z. Petri´cpetri´c, The typed Böhm teorem In Böhm theorem: applications to Computer Science Theory -BOTH, Electronic Notes in Theoretical Computer Science, vol.50, issue.2, p.13, 2001.

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 and D. Friedman, Control operators, the secd machine , and the lambda-calculus. In Formal description of programming concepts-III, pp.193-217, 1986.

M. Felleisen, D. P. Friedman, E. Kohlbecker, and B. F. Duba, Reasoning with continuations, First Symposium on Logic and Computer Science, pp.131-141, 1986.

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

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

K. Fujita, A sound and complete cps-translation for lambda-mucalculus, TLCA, pp.120-134, 2003.

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

T. Hardin, L. Maranget, and B. Pagano, Functional back-ends within the lambda-sigma calculus, ICFP, pp.25-33, 1996.
URL : https://hal.archives-ouvertes.fr/inria-00073659

H. Herbelin, Séquents qu'on calcule: de l'interprétation du calcul des séquents comme calcul de ?-termes et comme calcul de stratégies gagnantes, Thèse de doctorat, 1995.

H. Herbelin, Games and weak-head reduction for classical PCF, Third International Conference on Typed Lambda Calculi and Applications, TLCA '97 Proceedings, volume 1210 of Lecture Notes in Computer Science, pp.214-230, 1997.
DOI : 10.1007/3-540-62688-3_38
URL : https://hal.archives-ouvertes.fr/inria-00381542

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

H. Herbelin, C'est maintenant qu'on calcule: au coeur de la dualité. HabilitationàHabilitation`Habilitationà diriger les recherches, 2005.

F. Gregory and . Johnson, Gl ? a denotational testbed with continuations and partial continuations as first-class objects, SIGPLAN '87: Papers of the Symposium on Interpreters and interpretive techniques, pp.165-176, 1987.

F. Gregory, D. Johnson, and . Duggan, Stores and partial continuations as first-class objects in a language and its environment, POPL, pp.158-168, 1988.

T. Joly, Codages, séparabilité et représentation de fonctions dans divers ?-calculs typés, 2000.

Y. Kameyama and M. Hasegawa, A sound and complete axiomatization of delimited continuations, Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, pp.177-188, 2003.

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

C. Ong, A semantic view of classical proofs: type-theoretic, categorical, and denotational characterizations, Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, pp.230-241, 1996.
DOI : 10.1109/LICS.1996.561323

C. 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.215-227, 1997.
DOI : 10.1145/263699.263722

L. Paolini, Call-by-Value Separability and Computability, 7th Italian Conference Theoretical Computer Science, ICTCS'05, pp.74-89, 2001.
DOI : 10.1007/3-540-45446-2_5

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.

D. Pym and E. Ritter, On the semantics of classical disjunction, Journal of Pure and Applied Algebra, vol.159, issue.2-3, pp.315-338, 2001.
DOI : 10.1016/S0022-4049(00)00161-4

A. Sabry, Note on axiomatizing the semantics of control operators, 1996.

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

A. Saurin, Separation with streams in the ?µ-calculus, Proceedings, 20th Annual IEEE Symposium on Logic in Computer Science (LICS '05), pp.356-365, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00527871

A. Saurin, Typing streams in the lambda-mu-calculus, 14th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR '07), Lecture Notes in Artificial Intelligence, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00527835

P. Selinger, Control categories and duality: on the categorical semantics of the lambda-mu calculus, Mathematical Structures in Computer Science, vol.11, issue.2, pp.207-260, 2001.
DOI : 10.1017/S096012950000311X

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

A. K. Simpson, Categorical completeness results for the simply-typed lambda-calculus, Typed Lambda Calculus and Applications TLCA'95, pp.414-427, 1995.
DOI : 10.1007/BFb0014068

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
DOI : 10.1145/91556.91626

R. Statman, Completeness, invariance and ??-definability, The Journal of Symbolic Logic, vol.344, issue.01, pp.17-26, 1982.
DOI : 10.1016/0304-3975(76)90021-9