Cut elimination in multifocused linear logic

MaRDI QIDQ5015210zbMATH OpenFDO

Authors Taus Brock-Nannestad, Nicolas Guenot

Publication date 6 December 2021

Full work available at URL https://arxiv.org/abs/1502.04771, http://eptcs.web.cse.unsw.edu.au/paper.cgi?LINEARITY2014.3

Mathematics Subject Classification ID

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

Recommendations

• Multi-focused cut elimination
• From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
• On the computational complexity of cut-elimination in linear logic.
• Focusing and polarization in linear, intuitionistic, and classical logics
• Mechanizing focused linear logic in Coq

Cites work

• Focused natural deduction
• Focusing Strategies in the Sequent Calculus of Synthetic Connectives
• From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
• scientific article; zbMATH DE number 937366 (Why is no real title available?)
• Linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• On the unity of duality
• Proof nets, garbage, and computations
• Structural focalization
• The focused calculus of structures

Cited in

(5)

• Multi-focused proofs with different polarity assignments
• On concurrent behaviors and focusing in linear logic
• From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
• Multi-focused cut elimination
• scientific article; zbMATH DE number 7471682 (Why is no real title available?)

This page was built for publication: Cut elimination in multifocused linear logic

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