M. Zena, H. Ariola, and . Herbelin, Minimal classical logic and control operators, ICALP '03, pp.871-885, 2003.

Z. M. Ariola, H. Herbelin, and A. Sabry, A type-theoretic foundation of continuations and prompts, Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming (ICFP), pp.40-53, 2004.

D. Breazu-tannen, L. Kesner, and . Puel, A typed pattern calculus, [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pp.262-274, 1993.
DOI : 10.1109/LICS.1993.287581

[. Curien and H. Herbelin, The duality of computation, ACM SIGPLAN Notices, vol.35, issue.9, pp.233-243, 2000.
DOI : 10.1145/357766.351262
URL : https://hal.archives-ouvertes.fr/inria-00156377

H. Pierre-louis-curien, G. Herbelin, ?. Munch, and . Maccagnoni, The duality of computation under focus, 2009.

J. Vincent-danos, H. Joinet, and . Schellinx, A new deconstructive logic : Linear logic, 1995.

A. Filinski, Declarative continuations and categorical duality, 1989.
DOI : 10.1007/bfb0018355

[. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00075966

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

[. Girard, Le Point Aveugle, Cours de logique, Tome I : Vers la Perfection, Vision des Sciences, 2006.

[. Girard, Le Point Aveugle, Cours de logique, Tome II : Vers l'imperfection. Visions des Sciences, 2007.

[. Girard, P. Taylor, and Y. Lafont, Proofs and Types, 1989.

[. Herbelin, Duality of computation and sequent calculus : a few more remarks, 2008.

[. Krivine, Lambda-calcul, types et modèles, 1990.

[. Krivine, Lambda-calculus, types and models, 1993.
URL : https://hal.archives-ouvertes.fr/cel-00574575

[. Krivine, Realizability in classical logic, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00154500

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

D. Gordon and . Plotkin, Call-by-name, call-byvalue and the [lambda]-calculus, Theoretical Computer Science, vol.1, issue.2, pp.125-159, 1975.

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

[. Selinger, Some remarks on control categories, 2003.

A. Sabry and M. Felleisen, Reasoning about programs in continuationpassing style, Lisp and Symbolic Computation, pp.288-298, 1993.

[. Wadler, Call-by-value is dual to call-by-name, ACM SIGPLAN Notices, vol.38, issue.9, pp.189-201, 2003.
DOI : 10.1145/944746.944723

[. Wadler, Down with the bureaucracy of syntax ! pattern matching for classical linear logic, 2004.

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

[. Zeilberger, Refinement types and computational duality, Proceedings of the 3rd workshop on Programming languages meets program verification, PLPV '09, 2008.
DOI : 10.1145/1481848.1481852
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.188.2998