[. Accattoli and G. Guerrieri, Open call-by-value, Programming Languages and Systems, p.47, 2016.

N. Alechina, M. Mendler, E. Valeria-de-paiva, and . Ritter, Categorical and Kripke Semantics for Constructive S4 Modal Logic, Proc. CSL, pp.292-307, 2001.
DOI : 10.1007/3-540-44802-0_21

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

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

R. Atkey, Substructural simple type theories for separation and in-place update

D. Baelde, A. Doumane, and A. Saurin, Infinitary proof theory: the multiplicative additive case, Proc. CSL, p.47, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01339037

G. Bierman, 10 [BNG15] Taus Brock-Nannestad and Nicolas Guenot, Focused linear logic and the -calculus, Proc. TLCA, pp.78-93, 1995.

T. Brock-nannestad, N. Guenot, and D. Gustafsson, Computation in focused intuitionistic logic, Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, PPDP '15, pp.43-54, 2015.
DOI : 10.1145/2790449.2790528

URL : https://hal.archives-ouvertes.fr/hal-01249216

P. Curien, M. Fiore, and G. Munch-maccagnoni, A Theory of Effects and Resources: Adjunction Models and Polarised Calculi, Proc. POPL, p.46, 2006.
URL : https://hal.archives-ouvertes.fr/hal-01256092

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

K. Chaudhuri, D. Miller, and A. Saurin, Canonical sequent proofs via multifocusing , Fifth Ifip International Conference On Theoretical Computer Science?Tcs, pp.383-396, 2008.

B. Day, On closed categories of functors, Lecture Notes in Mathematics, issue.137, pp.1-38, 1970.

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

B. Day and S. Lack, Limits of small functors, Journal of Pure and Applied Algebra, vol.210, issue.3, pp.651-663, 2007.
DOI : 10.1016/j.jpaa.2006.10.019

[. Felleisen, On the expressive power of programming languages, Science of Computer Programming, vol.17, issue.1-3, pp.35-75, 1991.
DOI : 10.1016/0167-6423(91)90036-W

J. Girard, Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur, Gir91] _ , A new constructive logic: Classical logic, pp.37-38, 1972.

[. and L. P. Aveugle, Cours de logique, Tome II: Vers l'imperfection, Visions des Sciences, Hermann, 2007.

J. Krivine, Lambda-calculus, types and models, Ellis Horwood, Realizability in Classical Logic, pp.37-197, 1993.

O. Laurent, A proof of the focalization property of linear logic, lecture notes, p.45, 2004.

L. Paul-blain, Adjunction models for Call-by-Push-Value with stacks, Theory and Applications of Categories, vol.14, issue.5, pp.75-110, 2005.

C. Liang and D. Miller, Focusing and Polarization in Intuitionistic Logic, CSL, linear, intuitionistic, and classical logics, pp.451-465, 2007.
DOI : 10.1007/978-3-540-74915-8_34

URL : http://arxiv.org/abs/0708.2252

P. Melliès, Categorical semantics of linear logic, Panoramas et Synthèses, Maccagnoni, Focalisation and Classical Realisability Proc. CSL, pp.10-15, 2009.

A. Schalk, Whats is a categorical model of linear logic, p.10, 2004.

G. Scherer, Multi-focusing on extensional rewriting with sums, 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015 LIPIcs Schloss Dagstuhl -Leibniz- Zentrum fuer Informatik, pp.317-331, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01235372

R. J. Simmons, Structural Focalization, ACM Transactions on Computational Logic, vol.15, issue.3, pp.1-2133, 2014.
DOI : 10.1145/2629678

URL : http://arxiv.org/abs/1109.6273

V. Van, O. , and F. Van-raamsdonk, Weak Orthogonality Implies Confluence: The Higher Order Case, Proc. LFCS Femke van Raamsdonk, Higher-order Rewriting, Proc. Rewrit. Tech. App, pp.379-392, 1994.

[. Wadler, Call-by-value is dual to call-by-name, SIGPLAN Not, pp.189-201, 2003.
DOI : 10.1145/944705.944723