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

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

V. Beffara and . Danos, Disjunctive normal forms and local exceptions, ACM SIGPLAN Int. Conf. Func. Prog, pp.203-211, 2003.
DOI : 10.1145/944705.944724
URL : https://hal.archives-ouvertes.fr/hal-00009191

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

[. Curien and G. Munch-maccagnoni, The Duality of Computation under Focus, IFIP TCS, 2010.
DOI : 10.1007/978-3-642-15240-5_13
URL : https://hal.archives-ouvertes.fr/hal-01054461

J. Vincent-danos, H. Joinet, and . Schellinx, Abstract, Proceedings of the 2nd Conference on Computability in Europe (CiE'06), pp.755-807, 1995.
DOI : 10.1007/BF00885763

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

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

J. Girard, On the unity of logic, Annals of Pure and Applied Logic, vol.59, issue.3, pp.201-217301, 1993.
DOI : 10.1016/0168-0072(93)90093-S
URL : https://hal.archives-ouvertes.fr/inria-00075095

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

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

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

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

S. Lengrand and A. Miquel, Classical <mml:math altimg="si1.gif" display="inline" overflow="scroll" xmlns:xocs="http://www.elsevier.com/xml/xocs/dtd" xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns="http://www.elsevier.com/xml/ja/dtd" xmlns:ja="http://www.elsevier.com/xml/ja/dtd" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:tb="http://www.elsevier.com/xml/common/table/dtd" xmlns:sb="http://www.elsevier.com/xml/common/struct-bib/dtd" xmlns:ce="http://www.elsevier.com/xml/common/dtd" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:cals="http://www.elsevier.com/xml/common/cals/dtd"><mml:msub><mml:mrow><mml:mi>F</mml:mi></mml:mrow><mml:mrow><mml:mi>??</mml:mi></mml:mrow></mml:msub></mml:math>, orthogonality and symmetric candidates, Annals of Pure and Applied Logic, vol.153, issue.1-3, pp.3-20, 2008.
DOI : 10.1016/j.apal.2008.01.005

[. Nipkow, Higher-order critical pairs, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.342-349, 1991.
DOI : 10.1109/LICS.1991.151658

P. Wadler, Call-by-value is dual to call-by-name, Zei08] Noam Zeilberger. On the unity of duality. Ann. Pure and App. LogicZei09] Noam Zeilberger. Refinement types and computational duality. PLPV '09, pp.189-201, 2003.
DOI : 10.1145/944746.944723