@article(Bierman96,
 author       = {G.M. Bierman},
 year         = {1996},
 title        = {A note on full intuitionistic linear logic},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {79},
 number       = {3},
 pages        = {281 -- 287},
 doi          = {10.1016/0168-0072(96)00004-8},
)
@techreport(Brauener96,
 author       = {Torben Bra{\"u}ner and Valeria de Paiva},
 year         = {1996},
 title        = {Cut-Elimination for Full Intuitionistic Linear Logic},
 type         = {Technical Report},
 number       = {BRICS-RS-96-10},
 institution  = {BRICS, Aarhus, Danemark},
 note         = {Also available as Technical Report 395, Computer Laboratory, University of Cambridge},
)
@article(brighton15,
 author       = {Jude Brighton},
 year         = {2015},
 title        = {{Cut Elimination for GLS Using the Terminability of its Regress Process}},
 journal      = {Journal of Philosophical Logic},
 volume       = {45},
 doi          = {10.1007/s10992-015-9368-4},
)
@article(ChaudhuriTCS17,
 author       = {Kaustuv Chaudhuri and Leonardo Lima and Giselle Reis},
 year         = {2017},
 title        = {{Formalized Meta-Theory of Sequent Calculi for Substructural Logics}},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {332},
 pages        = {57 -- 73},
 doi          = {10.1016/j.entcs.2017.04.005},
 note         = {LSFA 2016 - 11th Workshop on Logical and Semantic Frameworks with Applications (LSFA)},
)
@article(phoas,
 author       = {Adam Chlipala},
 year         = {2008},
 title        = {Parametric Higher-Order Abstract Syntax for Mechanized Semantics},
 journal      = {SIGPLAN Not.},
 volume       = {43},
 number       = {9},
 pages        = {143\IeC{\textendash}156},
 doi          = {10.1145/1411203.1411226},
)
@inproceedings(dabrera21,
 author       = {Caitlin D'Abrera and Jeremy Dawson and Rajeev Gor\'{e}},
 year         = {2021},
 title        = {{A formally verified cut-elimination procedure for linear nested sequents for tense logic}},
 booktitle    = {28$^{th}$ International Conference on Automated Deduction (CADE-28)},
 note         = {Accepted for publication},
)
@inproceedings(Dawson10,
 author       = {Jeremy E. Dawson and Rajeev Gor{\'{e}}},
 year         = {2010},
 title        = {Generic Methods for Formalising Sequent Calculi Applied to Provability Logic},
 booktitle    = {Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings},
 pages        = {263--277},
 doi          = {10.1007/978-3-642-16242-8_19},
)
@inproceedings(EbnerIJCAR16,
 author       = {Gabriel Ebner and Stefan Hetzl and Giselle Reis and Martin Riener and Simon Wolfsteiner and Sebastian Zivota},
 year         = {2016},
 title        = {{System Description: GAPT 2.0}},
 booktitle    = {8$^{th}$ International Joint Conference on Automated Reasoning, (IJCAR)},
 pages        = {293--301},
 doi          = {10.1007/978-3-319-40229-1_20},
)
@unpublished(OlarteMSCS21,
 author       = {Amy Felty and Carlos Olarte and Bruno Xavier},
 year         = {2021},
 title        = {{A Focused Linear Logical Framework and its Application to Metatheory of Object Logics}},
 note         = {Submitted to MSCS},
)
@article(hybrid,
 author       = {Amy P. Felty and Alberto Momigliano},
 year         = {2012},
 title        = {{Hybrid - A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax}},
 journal      = {J. Autom. Reason.},
 volume       = {48},
 number       = {1},
 pages        = {43--105},
 doi          = {10.1007/s10817-010-9194-x},
)
@article(bindersChallenge2,
 author       = {Amy P. Felty and Alberto Momigliano and Brigitte Pientka},
 year         = {2015},
 title        = {The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations - Part 2 - {A} Survey},
 journal      = {J. Autom. Reason.},
 volume       = {55},
 number       = {4},
 pages        = {307--372},
 doi          = {10.1007/s10817-015-9327-3},
)
@article(bindersChallenge1,
 author       = {Amy P. Felty and Alberto Momigliano and Brigitte Pientka},
 year         = {2015},
 title        = {The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 1-A Common Infrastructure for Benchmarks},
 journal      = {CoRR},
 volume       = {abs/1503.06095},
)
@article(bindersBenchmark,
 author       = {Amy P. Felty and Alberto Momigliano and Brigitte Pientka},
 year         = {2018},
 title        = {Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions},
 journal      = {Math. Struct. Comput. Sci.},
 volume       = {28},
 number       = {9},
 pages        = {1507--1540},
 doi          = {10.1017/S0960129517000093},
)
@inproceedings(bindersComparison,
 author       = {Amy P. Felty and Brigitte Pientka},
 year         = {2010},
 title        = {Reasoning with Higher-Order Abstract Syntax and Contexts: {A} Comparison},
 editor       = {Matt Kaufmann and Lawrence C. Paulson},
 booktitle    = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {6172},
 publisher    = {Springer},
 pages        = {227--242},
 doi          = {10.1007/978-3-642-14052-5\_17},
)
@incollection(gentzen35,
 author       = {Gerhard Gentzen},
 year         = {1969},
 title        = {Investigations into Logical Deduction},
 editor       = {M. E. Szabo},
 booktitle    = {{The Collected Papers of Gerhard Gentzen}},
 publisher    = {North-Holland},
 address      = {Amsterdam},
 pages        = {68--131},
 note         = {Translation of articles that appeared in 1934-35},
)
@article(Gore12,
 author       = {Rajeev Gor\'{e} and Revantha Ramanayake},
 year         = {2012},
 title        = {Valentini's cut-elimination for provability logic resolved},
 journal      = {The Review of Symbolic Logic},
 volume       = {5},
 pages        = {212--238},
 doi          = {10.1017/S1755020311000323},
 url          = {http://journals.cambridge.org/article_S1755020311000323},
)
@inproceedings(gore21,
 author       = {Rajeev Gor\'{e} and Revantha Ramanayake and Ian Shillito},
 year         = {2021},
 title        = {{Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq}},
 booktitle    = {28$^{th}$ International Conference on Automated Deduction (CADE-28)},
 note         = {Accepted for publication},
)
@phdthesis(lengrand14,
 author       = {Graham-Lengrand, {St\'ephane}},
 year         = {2014},
 title        = {Polarities \& Focussing: a journey from Realisability to Automated Reasoning},
 type         = {Habilitation thesis},
 school       = {Universit{\'e} {Paris-Sud}},
)
@article(lf93,
 author       = {Robert Harper and Furio Honsell and Gordon Plotkin},
 year         = {1993},
 title        = {A Framework for Defining Logics},
 journal      = {J. ACM},
 volume       = {40},
 number       = {1},
 pages        = {143\IeC{\textendash}184},
 doi          = {10.1145/138027.138060},
)
@inproceedings(lns,
 author       = {Bjoern Lellmann and Carlos Olarte and Elaine Pimentel},
 year         = {2017},
 title        = {{A uniform framework for substructural logics with modalities}},
 editor       = {Thomas Eiter and David Sands},
 booktitle    = {LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
 series       = {EPiC Series in Computing},
 volume       = {46},
 publisher    = {EasyChair},
 pages        = {435--455},
 doi          = {10.29007/93qg},
)
@inproceedings(Marin14,
 author       = {Sonia Marin and Stra{\ss}burger, Lutz},
 year         = {2014},
 title        = {Label-free Modular Systems for Classical and Intuitionistic Modal Logics},
 booktitle    = {Advances in Modal Logic 10, invited and contributed papers from the tenth conference on "Advances in Modal Logic," held in Groningen, The Netherlands, August 5-8, 2014},
 pages        = {387--406},
)
@article(two-level,
 author       = {Raymond C. McDowell and Dale A. Miller},
 year         = {2002},
 title        = {{Reasoning with Higher-Order Abstract Syntax in a Logical Framework}},
 journal      = {ACM Trans. Comput. Logic},
 volume       = {3},
 number       = {1},
 pages        = {80\IeC{\textendash}136},
 doi          = {10.1145/504077.504080},
)
@article(llinda,
 author       = {Dale Miller and Elaine Pimentel},
 year         = {2013},
 title        = {A formal framework for specifying sequent calculus proof systems},
 journal      = {Theoretical Computer Science},
 volume       = {474},
 pages        = {98--116},
 doi          = {10.1016/j.tcs.2012.12.008},
)
@phdthesis(nigam09phd,
 author       = {Vivek Nigam},
 year         = {2009},
 title        = {Exploiting non-canonicity in the {S}equent {C}alculus},
 school       = {Ecole Polytechnique},
)
@article(NigamJLC16,
 author       = {Vivek Nigam and Elaine Pimentel and Giselle Reis},
 year         = {2016},
 title        = {{An extended framework for specifying and reasoning about proof systems}},
 journal      = {Journal of Logic and Computation},
 volume       = {26},
 number       = {2},
 pages        = {539--576},
 doi          = {10.1093/logcom/exu029},
)
@inproceedings(NigamTPLP13,
 author       = {Vivek Nigam and Giselle Reis and Leonardo Lima},
 year         = {2013},
 title        = {{Checking Proof Transformations with ASP}},
 booktitle    = {29$^{th}$ International Conference on Logic Programming (ICLP)},
 volume       = {13},
)
@inproceedings(NigamIJCAR2014,
 author       = {Vivek Nigam and Giselle Reis and Leonardo Lima},
 year         = {2014},
 title        = {{Quati: An Automated Tool for Proving Permutation Lemmas}},
 booktitle    = {7$^{th}$ International Joint Conference on Automated Reasoning (IJCAR 2014)},
 pages        = {255--261},
 doi          = {10.1007/978-3-319-08587-6_18},
)
@inproceedings(OlarteRLA18,
 author       = {Carlos Olarte and Elaine Pimentel and Camilo Rocha},
 year         = {2018},
 title        = {Proving Structural Properties of Sequent Systems in Rewriting Logic},
 editor       = {Vlad Rusu},
 booktitle    = {Rewriting Logic and Its Applications - 12th International Workshop, {WRLA} 2018, Held as a Satellite Event of ETAPS, Thessaloniki, Greece, June 14-15, 2018, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {11152},
 publisher    = {Springer},
 pages        = {115--135},
 doi          = {10.1007/978-3-319-99840-4\_7},
)
@inproceedings(Pinto09,
 author       = {Lu{\'i}s Pinto and Tarmo Uustalu},
 year         = {2009},
 title        = {Proof Search and Counter-Model Construction for Bi-intuitionistic Propositional Logic with Labelled Sequents},
 editor       = {Martin Giese and Arild Waaler},
 booktitle    = {Automated Reasoning with Analytic Tableaux and Related Methods: 18th International Conference, TABLEAUX 2009, Oslo, Norway, July 6-10, 2009. Proceedings},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {295--309},
 doi          = {10.1007/978-3-642-02716-1_22},
)
@inproceedings(Sequoia,
 author       = {Giselle Reis and Zan Naeem and Mohammed Hashim},
 year         = {2020},
 title        = {{Sequoia: A Playground for Logicians}},
 editor       = {Nicolas Peltier and Sofronie-Stokkermans, Viorica},
 booktitle    = {10$^{th}$ International Joint Conference on Automated Reasoning, (IJCAR)},
 publisher    = {Springer International Publishing},
 pages        = {480--488},
 doi          = {10.1007/978-3-030-51054-1_32},
)
@inproceedings(Tews13,
 author       = {Hendrik Tews},
 year         = {2013},
 title        = {Formalizing Cut Elimination of Coalgebraic Logics in Coq},
 editor       = {Didier Galmiche and Larchey-Wendling, Dominique},
 booktitle    = {Automated Reasoning with Analytic Tableaux and Related Methods: 22nd International Conference, TABLEAUX 2013, Nancy, France, September 16-19, 2013, Proceedings},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {257--272},
 doi          = {10.1007/978-3-642-40537-2_22},
)
@inproceedings(Urban08,
 author       = {Christian Urban and Bozhi Zhu},
 year         = {2008},
 title        = {Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof},
 editor       = {Andrei Voronkov},
 booktitle    = {Rewriting Techniques and Applications: 19th International Conference, RTA 2008 Hagenberg, Austria, July 15-17, 2008 Proceedings},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {409--424},
 doi          = {10.1007/978-3-540-70590-1_28},
)
@article(OlarteLSFA17,
 author       = {Bruno Xavier and Carlos Olarte and Giselle Reis and Vivek Nigam},
 year         = {2018},
 title        = {{Mechanizing Focused Linear Logic in Coq}},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {338},
 pages        = {219 -- 236},
 doi          = {10.1016/j.entcs.2018.10.014},
 note         = {The 12th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2017)},
)