B. Accattoli, P. Barenbaum, and D. Mazza, Distilling abstract machines, pp.363-376, 2014.

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

Z. Ariola, A. Bohannon, and A. Sabry, Sequent calculi and abstract machines, ACM Transactions on Programming Languages and Systems, vol.31, issue.4, 2009.
DOI : 10.1145/1516507.1516508

D. Baelde and D. Miller, Least and greatest fixed points in linear logic Barendregt and S. Ghilezan. Lambda-terms for natural deduction, sequent calculus and cut elimination, LNCS Journal of Functional Programming, vol.4790, issue.101, pp.92-106121, 2000.

T. Brock-nannestad and C. Schürmann, Focused Natural Deduction, LNCS, vol.6397, issue.17, pp.157-171, 2010.
DOI : 10.1007/978-3-642-16242-8_12

K. Chaudhuri, Classical and Intuitionistic Subexponential Logics Are Equally Expressive, LNCS, vol.6247, issue.10, pp.185-199, 2010.
DOI : 10.1007/978-3-642-15205-4_17
URL : https://hal.archives-ouvertes.fr/inria-00534865

K. Chaudhuri, N. Guenot, and L. Straßburger, The focused calculus of structures, LIPIcs, vol.12, issue.11, pp.159-173, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00772420

S. Cittadini and W. Sieg, Normal natural deduction proofs (in non-classical logics), Mechanizing Mathematical Reasoning, 2005.

P. Curien and H. Herbelin, The duality of computation, ICFP'00, pp.233-243, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00156377

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

V. Danos, J. Joinet, and H. Schellinx, LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication, Advances in Linear Logic, number 222 in LMS Lecture Note Series, pp.211-224, 1995.

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

R. Dyckhoff and S. Lengrand, LJQ: A Strongly Focused Calculus for Intuitionistic Logic, LNCS, vol.94, issue.06, pp.173-185, 2006.
DOI : 10.1090/trans2/094/02
URL : https://hal.archives-ouvertes.fr/hal-00150287

J. and E. Santo, Completing Herbelin's programme, TLCA'07, pp.118-132, 2007.

J. and E. Santo, Delayed substitutions, RTA'07, pp.169-183, 2007.

J. and E. Santo, The ?-calculus and the unity of structural proof theory, Theory of Computing Systems, pp.963-994, 2009.

M. Felleisen and D. P. Friedman, Control operators, the SECD-machine and the ?-calculus, 1986.

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, pp.255-296, 1991.
DOI : 10.1016/0304-3975(87)90045-4

H. Herbelin, A ??-calculus structure isomorphic to Gentzen-style sequent calculus structure, CSL'94, pp.61-75, 1994.
DOI : 10.1007/BFb0022247
URL : https://hal.archives-ouvertes.fr/inria-00381525

F. Joachimski and R. Matthes, Standardization and Confluence for a Lambda Calculus with Generalized Applications, LNCS, vol.1833, issue.00, pp.141-155, 2000.
DOI : 10.1007/10721975_10

J. Krivine, A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation, pp.199-207, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00154508

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

P. Levy, Call-by-push-value: Decomposing call-by-value and call-by-name. Higher-Order and Symbolic Computation, pp.377-414, 2006.
DOI : 10.1007/978-94-007-0954-6

C. Liang and D. Miller, Focusing and polarization in linear, intuitionistic, and classical logics, Theoretical Computer Science, vol.410, issue.46, pp.4747-4768, 2009.
DOI : 10.1016/j.tcs.2009.07.041

E. Moggi, Computational lambda-calculus and monads, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.14-23, 1989.
DOI : 10.1109/LICS.1989.39155

V. Nigam and E. Pimentel, Relating focused proofs with different polarity assignments, LFMTP'13, 2013.

R. Simmons, Structural Focalization, ACM Transactions on Computational Logic, vol.15, issue.3, p.21, 2014.
DOI : 10.1145/2629678

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