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

M. Boespflug, Conception d'un noyau de vérification de preuves pour le ??-calcul modulo, 2011.

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

K. Chaudhuri, The Focused Inverse Method for Linear Logic, 2006.

K. Chaudhuri, Focusing Strategies in the Sequent Calculus of Synthetic Connectives, LPAR: International Conference on Logic, Programming, pp.467-481, 2008.
DOI : 10.1007/978-3-540-89439-1_33

K. Chaudhuri, Magically Constraining the Inverse Method Using Dynamic Polarity Assignment, Proc. 17th Int. Conf. on Logic for Programming , Artificial Intelligence, and Reasoning (LPAR), pp.202-216, 2010.
DOI : 10.1007/978-3-642-16242-8_15
URL : https://hal.archives-ouvertes.fr/inria-00535948

K. Chaudhuri, N. Guenot, and L. Straßburger, The Focused Calculus of Structures, Computer Science Logic: 20th Annual Conference of the EACSL, Leibniz International Proceedings in Informatics (LIPIcs) Schloss Dagstuhl?Leibniz-Zentrum für Informatik, pp.159-173, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00772420

K. Chaudhuri, F. Pfenning, and G. Price, A Logical Characterization of Forward and Backward Chaining in the Inverse Method, Journal of Automated Reasoning, vol.2, issue.5, pp.133-177, 2008.
DOI : 10.1007/s10817-007-9091-0

R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, The Journal of Symbolic Logic, vol.475, issue.03, pp.795-807, 1992.
DOI : 10.1007/3-540-54487-9_58

J. Hodas and D. Miller, Logic Programming in a Fragment of Intuitionistic Linear Logic, Information and Computation, vol.110, issue.2, pp.327-365, 1994.
DOI : 10.1006/inco.1994.1036

J. Hodas, K. Watkins, N. Tamura, and K. Kang, Efficient implementation of a linear logic programming language, Proceedings of the 1998 Joint International Conference and Symposium on Logic Programming, pp.145-159, 1998.

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

O. Laurent, A proof of the focalization property of linear logic. Unpublished note, 2004.

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

P. Lincoln, J. Mitchell, A. Scedrov, and N. Shankar, Decision problems for propositional linear logic, Annals of Pure and Applied Logic, vol.56, issue.1-3, pp.239-311, 1992.
DOI : 10.1016/0168-0072(92)90075-B
URL : http://doi.org/10.1016/0168-0072(92)90075-b

D. Miller, A Proposal for Broad Spectrum Proof Certificates, CPP: First International Conference on Certified Programs and Proofs, pp.54-69, 2011.
DOI : 10.1007/978-3-540-88387-6_3
URL : https://hal.archives-ouvertes.fr/hal-00772722

D. Miller and A. Saurin, From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic, CSL 2007: Computer Science Logic, pp.405-419, 2007.
DOI : 10.1007/978-3-540-74915-8_31
URL : https://hal.archives-ouvertes.fr/hal-00527888

G. C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.106-119, 1997.
DOI : 10.1145/263699.263712

L. Straßburger, Linear Logic and Noncommutativity in the Calculus of Structures, 2003.