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