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

D. Marcello, M. Agostino, and . Mondadori, The taming of the cut. Classical refutations with analytic cut, J. of Logic and Computation, vol.4, issue.3, pp.285-319, 1994.

R. Dyckhoff and S. Lengrand, LJQ: A Strongly Focused Calculus for Intuitionistic Logic, LNCS, vol.94, pp.173-185, 2006.
DOI : 10.1090/trans2/094/02

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

A. Felty and D. Miller, Specifying theorem provers in a higherorder logic programming language, 9th Conference on Automated Deduction, pp.61-80, 1988.

G. Gentzen, Investigations into logical deductions The Collected Papers of Gerhard Gentzen, pp.68-131, 1969.

R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, 2nd Symp. on Logic in Computer Science, pp.194-204, 1987.
DOI : 10.1145/138027.138060

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

D. Miller, A multiple-conclusion meta-logic, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp.272-281, 1994.
DOI : 10.1109/LICS.1994.316062

D. Miller and E. Pimentel, Using Linear Logic to Reason about Sequent Systems, International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pp.2-23, 2002.
DOI : 10.1007/3-540-45616-3_2

D. Miller and E. Pimentel, Linear logic as a framework for specifying sequent calculus, Logic Colloquium '99: Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, pp.111-135, 2004.
DOI : 10.1017/9781316755921.010

V. Nigam and D. Miller, A Framework for Proof Systems, Journal of Automated Reasoning, vol.40, issue.7, 2009.
DOI : 10.1007/s10817-010-9182-1

M. Parigot, Free deduction: An analysis of ???Computations??? in classical logic, Proceedings of the First Russian Conference on Logic Programming, pp.361-380, 1992.
DOI : 10.1007/3-540-55460-2_27

F. Pfenning, Elf: a language for logic definition and verified metaprogramming, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.313-321, 1989.
DOI : 10.1109/LICS.1989.39186

F. Pfenning, Structural Cut Elimination, Information and Computation, vol.157, issue.1-2, pp.84-141, 2000.
DOI : 10.1006/inco.1999.2832

URL : http://doi.org/10.1006/inco.1999.2832

F. Pfenning, Automated theorem proving. Lecture notes, 2004.

E. Pimentel and D. Miller, On the Specification of Sequent Systems, 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, number 3835 in LNAI, pp.352-366, 2005.
DOI : 10.1007/11591191_25

E. Gouvêa-pimentel and M. G. Brasil, Lógica linear e a especificação de sistemas computacionais, 2001.

P. Schroeder-heister, A natural extension of natural deduction, The Journal of Symbolic Logic, vol.36, issue.04, pp.1284-1300, 1984.
DOI : 10.1007/978-94-009-9825-4_2

W. Sieg and J. Byrnes, Normal Natural Deduction Proofs (in Non-classical Logics), Studia Logica, vol.60, issue.1, pp.67-106, 1998.
DOI : 10.1007/978-3-540-32254-2_11

R. M. Smullyan, Analytic cut, The Journal of Symbolic Logic, vol.1, issue.04, pp.560-564, 1968.
DOI : 10.2307/2271362

P. Jan-von, Natural deduction with general elimination rules, Archive for Mathematical Logic, vol.40, issue.7, pp.541-567, 2001.