@article(andreoli92jlc,
 author       = {Jean-Marc Andreoli},
 year         = {1992},
 title        = {Logic Programming with Focusing Proofs in Linear Logic},
 journal      = {Journal of Logic and Computation},
 volume       = {2},
 number       = {3},
 pages        = {297--347},
 doi          = {10.1093/logcom/2.3.297},
)
@phdthesis(baelde08phd,
 author       = {David Baelde},
 year         = {2008},
 title        = {A linear approach to the proof-theory of least and greatest fixed points},
 school       = {Ecole Polytechnique},
)
@incollection(danos93wll,
 author       = {V. Danos and J.-B. Joinet and H. Schellinx},
 year         = {1995},
 title        = {{LKT} and {LKQ}: sequent calculi for second order logic based upon dual linear decompositions of classical implication},
 booktitle    = {Advances in Linear Logic},
 pages        = {211--224},
 doi          = {10.1017/CBO9780511629150.011},
)
@article(dyckhoff92jsl,
 author       = {Roy Dyckhoff},
 year         = {1992},
 title        = {Contraction-free sequent calculi for intuitionistic logic},
 journal      = {Journal of Symbolic Logic},
 volume       = {57},
 number       = {3},
 pages        = {795--807},
 doi          = {10.2307/2275431},
)
@inproceedings(liang07csl,
 author       = {Chuck Liang and Dale Miller},
 year         = {2007},
 title        = {Focusing and Polarization in Intuitionistic Logic},
 booktitle    = {Computer Science Logic},
 series       = {LNCS},
 volume       = {4646},
 publisher    = {Springer},
 pages        = {451--465},
 doi          = {10.1007/978-3-540-74915-8\_34},
)
@article(liang09tcs,
 author       = {Chuck Liang and Dale Miller},
 year         = {2009},
 title        = {Focusing and Polarization in Linear, Intuitionistic, and Classical Logics},
 journal      = {Theoretical Computer Science},
 volume       = {410},
 number       = {46},
 pages        = {4747--4768},
 doi          = {10.1016/j.tcs.2009.07.041},
)
@inproceedings(miller07cslb,
 author       = {Dale Miller and Alexis Saurin},
 year         = {2007},
 title        = {From proofs to focused proofs: a modular proof of focalization in Linear Logic},
 booktitle    = {CSL 2007},
 series       = {LNCS},
 pages        = {405--419},
 doi          = {10.1007/978-3-540-74915-8\_31},
)
@phdthesis(nigam09phd,
 author       = {Vivek Nigam},
 year         = {2009},
 title        = {Exploiting non-canonicity in the sequent calculus},
 school       = {Ecole Polytechnique},
)
@inproceedings(nigam13iclp,
 author       = {Vivek Nigam and Giselle Reis and Leonardo Lima},
 year         = {2013},
 title        = {Checking Proof Transformations with {ASP}},
 booktitle    = {ICLP (Technical Communications)},
 volume       = {13},
)
@inproceedings(nigam14ijcar,
 author       = {Vivek Nigam and Giselle Reis and Leonardo Lima},
 year         = {2014},
 title        = {Quati: An Automated Tool for Proving Permutation Lemmas},
 booktitle    = {7th {IJCAR} Proceedings},
 pages        = {255--261},
 doi          = {10.1007/978-3-319-08587-6\_18},
)
@phdthesis(saurin08phd,
 author       = {Alexis Saurin},
 year         = {2008},
 title        = {Une \'etude logique du contr\^ole (appliqu\'ee \`a\ la programmation fonctionnelle et logique)},
 school       = {Ecole Polytechnique},
)