A fresh view of linear logic as a logical framework

DOI10.1016/J.ENTCS.2020.08.008MaRDI QIDQ2229156zbMATH OpenOpenAlexWikidataFDO

Authors Carlos Olarte, Elaine Pimentel, Bruno Xavier

Publication date 22 February 2021

Full work available at URL https://doi.org/10.1016/j.entcs.2020.08.008

zbMATH Keywords

linear logiccut elimination

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Recommendations

• An extended framework for specifying and reasoning about proof systems
• On the Specification of Sequent Systems
• A framework for proof systems
• scientific article; zbMATH DE number 1950250
• A formal framework for specifying sequent calculus proof systems

Cites work

• scientific article; zbMATH DE number 1612551 (Why is no real title available?)
• scientific article; zbMATH DE number 956466 (Why is no real title available?)
• scientific article; zbMATH DE number 517072 (Why is no real title available?)
• scientific article; zbMATH DE number 1980939 (Why is no real title available?)
• scientific article; zbMATH DE number 1749009 (Why is no real title available?)
• scientific article; zbMATH DE number 7204444 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• A formal framework for specifying sequent calculus proof systems
• A framework for proof systems
• A proof theoretic view of spatial and temporal dependencies in biochemical systems
• A semantical view of proof systems
• A uniform framework for substructural logics with modalities
• An analysis of (linear) exponentials based on extended sequents
• An extended framework for specifying and reasoning about proof systems
• Deep sequent systems for modal logic
• Eine Darstellung der Intuitionistischen Logik in der Klassischen
• From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
• Linear Nested Sequents, 2-Sequents and Hypersequents
• Linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• Mechanizing focused linear logic in Coq
• Modularisation of sequent calculi for normal and non-normal modalities
• On subexponentials, focusing and modalities in concurrent systems
• Proof search in nested sequent calculi
• Sequentialising nested systems
• Structural cut elimination. I: Intuitionistic and classical logic
• Subexponentials in non-commutative linear logic
• The Method of Tree-Hypersequents for Modal Propositional Logic

Cited in

(8)

• A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems
• A linear logic framework for multimodal logics
• A formally verified cut-elimination procedure for linear nested sequents for tense logic
• A focused linear logical framework and its application to metatheory of object logics
• Some Syntactical Observations on Linear Logic
• On the Specification of Sequent Systems
• An extended framework for specifying and reasoning about proof systems
• A simplified account of the metatheory of linear LF

This page was built for publication: A fresh view of linear logic as a logical framework

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2229156)