From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic

DOI10.1007/978-3-540-74915-8_31MaRDI QIDQ3608427zbMATH OpenOpenAlexFDO

Authors Alexis Saurin, Dale Miller

Publication date 5 March 2009

Published in Computer Science Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-74915-8_31

Mathematics Subject Classification ID

Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Recommendations

• Structural focalization
• The focused calculus of structures
• Cut elimination in multifocused linear logic
• Focusing and polarization in linear, intuitionistic, and classical logics
• Logic Programming with Focusing Proofs in Linear Logic

Cited in

(24)

• Focusing and polarization in linear, intuitionistic, and classical logics
• A semantic framework for proof evidence
• From cut-free calculi to automated deduction: the case of bounded contraction
• A fresh view of linear logic as a logical framework
• Mechanizing focused linear logic in Coq
• On concurrent behaviors and focusing in linear logic
• On subexponentials, focusing and modalities in concurrent systems
• A framework for linear authorization logics
• A proof theoretic view of spatial and temporal dependencies in biochemical systems
• On the meaning of focalization
• From focalization of logic to the logic of focalization
• Axiom Directed Focusing
• Multi-focused cut elimination
• Expressing additives using multiplicatives and subexponentials
• Undecidability of multiplicative subexponential logic
• Cut elimination in multifocused linear logic
• A focused linear logical framework and its application to metatheory of object logics
• Yet another bijection between sequent calculus and natural deduction
• Proving concurrent constraint programming correct, revisited
• A linear logic framework for multimodal logics
• A proof of the focusing theorem via MALL proof nets
• Bracket induction for Lambek calculus with bracket modalities
• Sequent systems on undirected graphs
• Subexponential concurrent constraint programming

This page was built for publication: From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic

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