J. Andreoli, Logic Programming with Focusing Proofs in Linear Logic, Journal of Logic and Computation, vol.2, issue.3, pp.297-347, 1992.
DOI : 10.1093/logcom/2.3.297

P. Curien and H. Herbelin, The duality of computation, Proc. Int. Conf. on Functional Programming, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00156377

V. Danos, J. Joinet, and H. Schellinx, Abstract, The Journal of Symbolic Logic, vol.II, issue.03, 1997.
DOI : 10.1007/BF00885763
URL : https://hal.archives-ouvertes.fr/inria-00528352

O. Danvy, Back to direct style, Science of Computer Programming, vol.22, issue.3, pp.183-195, 1994.
DOI : 10.1016/0167-6423(94)00003-4

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. Girard, Locus solum: from the rules of logic to the logic of rules, Mathematical Structures in Computer Science, vol.11, issue.3, pp.301-506, 2001.

T. Griffin, A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '90, 1990.
DOI : 10.1145/96709.96714

H. Herbelin, C'est maintenant qu'on calcule, au coeur de la dualité, Mémoire d'habilitation, available from cited url, 2005.

J. Krivine, Lambda-calcul, types et modèles, 1991.

J. Krivine, A call-by-name lambda-calculus machine, Higher Order and Symbolic Computation, pp.199-207, 2007.

Y. Lafont, B. Reus, and T. Streicher, Continuation Semantics or Expressing Implication by Negation, 1993.

P. Landin, The Mechanical Evaluation of Expressions, The Computer Journal, vol.6, issue.4, pp.308-320, 1964.
DOI : 10.1093/comjnl/6.4.308

O. Laurent, Etude de la polarisation en logique, Thèse de Doctorat, 2002.
URL : https://hal.archives-ouvertes.fr/tel-00007884

O. Laurent, M. Quatrini, and L. , Tortora de Falco, Polarised and focalised linear and classical proofs, Ann. of Pure and Appl. Logic, vol.134, pp.2-3217, 2005.
DOI : 10.1016/j.apal.2004.11.002
URL : http://doi.org/10.1016/j.apal.2004.11.002

P. B. Levy, Call-by-push-value. A functional/imperative synthesis, Semantic Structures in Computation, 2004.
DOI : 10.1007/978-94-007-0954-6

G. Munch-maccagnoni, Focalisation and Classical Realisability, Proc. CSL, pp.409-423, 2009.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00409793

C. Murthy, A computational analysis of Girard's translation and LC, [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, 1992.
DOI : 10.1109/LICS.1992.185523

T. Nipkow, Orthogonal higher-order rewriting systems are confluent, Proc. TLCA, 1993.
DOI : 10.1007/bfb0037114

L. Ong and C. 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
DOI : 10.1145/263699.263722

M. Parigot, ?µ-calculus: An algorithmic interpretation of classical natural deduction, Proc. LPAR, St. Petersburg, 1992.

G. Plotkin, Call-by-name, call-by-value and the ??-calculus, Theoretical Computer Science, vol.1, issue.2, pp.125-159, 1975.
DOI : 10.1016/0304-3975(75)90017-1

M. Quatrini and L. , Tortora de Falco, Polarisation des preuves classiques et renversement, pp.113-116, 1996.

. Ph and . Wadler, Call-by-value is dual to call-by-name, Proc. ICFP, 2003.

N. Zeilberger, On the unity of duality, Annals of Pure and Applied Logic, vol.153, issue.1-3, pp.66-96, 2008.
DOI : 10.1016/j.apal.2008.01.001