Maximally multi-focused proofs for skew non-commutative \texttt{MILL}

DOI10.1007/978-3-031-39784-4_24MaRDI QIDQ6199592

Niccolò Veltri

Publication date: 28 February 2024

Published in: Logic, Language, Information, and Computation (Search for Journal in Brave)

zbMATH Keywords

substructural logicsAgdamaximal multi-focusingskew monoidal closed categoriesskew non-commutative MILL

Mathematics Subject Classification ID

Logic in computer science (03B70)

Cites Work

• Unnamed Item
• Unnamed Item
• Linear logic
• Focusing and polarization in linear, intuitionistic, and classical logics
• Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic
• Multi-focused proofs with different polarity assignments
• Coherence via focusing for symmetric skew monoidal categories
• Skew-closed categories
• Which simple types have a unique inhabitant?
• Logic Programming with Focusing Proofs in Linear Logic
• Multi-focused cut elimination
• The Sequent Calculus of Skew Monoidal Categories
• Monads need not be endofunctors
• A multi-focused proof system isomorphic to expansion proofs