Jean-Marc Andreoli (1992):
Logic Programming with Focusing Proofs in Linear Logic.
Journal of Logic and Computation 2(3),
pp. 297–347,
doi:10.1093/logcom/2.3.297.
David Baelde (2008):
A linear approach to the proof-theory of least and greatest fixed points.
Ecole Polytechnique.
V. Danos, J.-B. Joinet & H. Schellinx (1995):
LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication.
In: Advances in Linear Logic,
pp. 211–224,
doi:10.1017/CBO9780511629150.011.
Roy Dyckhoff (1992):
Contraction-free sequent calculi for intuitionistic logic.
Journal of Symbolic Logic 57(3),
pp. 795–807,
doi:10.2307/2275431.
Chuck Liang & Dale Miller (2007):
Focusing and Polarization in Intuitionistic Logic.
In: Computer Science Logic,
LNCS 4646.
Springer,
pp. 451–465,
doi:10.1007/978-3-540-74915-8_34.
Chuck Liang & Dale Miller (2009):
Focusing and Polarization in Linear, Intuitionistic, and Classical Logics.
Theoretical Computer Science 410(46),
pp. 4747–4768,
doi:10.1016/j.tcs.2009.07.041.
Dale Miller & Alexis Saurin (2007):
From proofs to focused proofs: a modular proof of focalization in Linear Logic.
In: CSL 2007,
LNCS,
pp. 405–419,
doi:10.1007/978-3-540-74915-8_31.
Vivek Nigam (2009):
Exploiting non-canonicity in the sequent calculus.
Ecole Polytechnique.
Vivek Nigam, Giselle Reis & Leonardo Lima (2013):
Checking Proof Transformations with ASP.
In: ICLP (Technical Communications) 13.
Vivek Nigam, Giselle Reis & Leonardo Lima (2014):
Quati: An Automated Tool for Proving Permutation Lemmas.
In: 7th IJCAR Proceedings,
pp. 255–261,
doi:10.1007/978-3-319-08587-6_18.
Alexis Saurin (2008):
Une étude logique du contrôle (appliquée à la programmation fonctionnelle et logique).
Ecole Polytechnique.