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, H. Herbelin, and A. Sabry, A Type-Theoretic Foundation of Continuations and Prompts, ACM SIGPLAN International Conference on Functional Programming, pp.40-53, 2004.

Z. M. Ariola, H. Herbelin, and A. Sabry, A Proof-Theoretic Foundation of Abortive Continuations (Extended version, 2005.

A. Avron, Natural 3-valued logics???characterization and proof theory, The Journal of Symbolic Logic, vol.31, issue.01, pp.276-294, 1991.
DOI : 10.1016/0304-3975(87)90045-4

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

H. P. Barendregt, Lambda Calculi with Types Handbook of Logic in, Computer Science, vol.2, pp.117-309, 1992.

G. Bierman, A Computational Interpretation of the lambda-mu calculus, Mathematical foundations of computer science, LNCS 1450, pp.336-345, 1998.

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. 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.

P. De-groote, An environment machine for the ????-calculus, Mathematical Structures in Computer Science, vol.8, issue.6, pp.637-669, 1998.
DOI : 10.1017/S0960129598002667
URL : https://hal.archives-ouvertes.fr/inria-00098499

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 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

G. Gentzen, Investigations into logical deduction Collected papers of Gerhard Gentzen, pp.68-131, 1969.

J. Girard, A new constructive logic: classic logic, Mathematical Structures in Computer Science, vol.7, issue.2, pp.255-296, 1991.
DOI : 10.1016/0304-3975(87)90045-4

J. Goubault-larrecq and I. Mackie, Proof Theory and Automated Deduction, 2001.
DOI : 10.1007/978-94-011-3981-6

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

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

I. Johansson, Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus, Compositio Math, vol.4, pp.119-136, 1937.

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.

R. Lalement, Computation as Logic, 1993.

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.

M. Parigot, Classical proofs as programs'. Computational logic and theory 713, pp.263-276, 1993.
DOI : 10.1007/bfb0022575

M. Parigot, Strong normalization for second order classical natural deduction, [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pp.39-47, 1993.
DOI : 10.1109/LICS.1993.287602

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

D. Prawitz, Natural Deduction, a Proof-Theoretical Study, Almquist and Wiksell, 1965.

W. Py, Confluence en ?µ-calcul, 1998.

A. Sabry and M. Felleisen, Reasoning about programs in continuation-passing style, Lisp Symb. Comput, vol.6, pp.3-4, 1993.

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

T. Streicher and B. Reus, Classical logic, continuation semantics and abstract machines, Journal of Functional Programming, vol.8, issue.6, pp.543-572, 1998.
DOI : 10.1017/S0956796898003141

D. Van-dalen, Logic and Structure, 1997.