Bunched logics displayed

DOI10.1007/S11225-012-9449-0MaRDI QIDQ1935559zbMATH OpenOpenAlexFDO

Authors James Brotherston

Publication date 18 February 2013

Published in Studia Logica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s11225-012-9449-0

zbMATH Keywords

proof theorycut eliminationbunched logicdisplay calculus

Mathematics Subject Classification ID

Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Cut-elimination and normal-form theorems (03F05)

Recommendations

• A unified display proof theory for bunched logic
• Bunched hypersequent calculi for distributive substructural logics
• Classical BI: Its Semantics and Proof Theory
• A labelled sequent calculus for BBI: proof theory and proof search
• scientific article; zbMATH DE number 966898

Cites work

• scientific article; zbMATH DE number 970628 (Why is no real title available?)
• A unified display proof theory for bunched logic
• BI as an assertion language for mutable data structures
• Bunched polymorphism
• Classical BI
• Classical BI: Its Semantics and Proof Theory
• Constructive negation, implication, and co-implication
• Context logic as modal logic, completeness and parametric inexpressivity
• Decision problems for propositional linear logic
• Display logic
• Displaying and deciding substructural logics. I: Logics with contraposition
• Enhancing modular OO verification with separation logic
• Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding
• Expressivity Properties of Boolean BI Through Relational Models
• From IF to BI. A tale of dependence and separation
• Gaggles, Gentzen and Galois: how to display your favourite substructural logic
• Logical Approaches to Computational Barriers
• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• Relational inductive shape analysis
• Strong update, disposal, and encapsulation in bunched typing
• The Logic of Bunched Implications
• The semantics and proof theory of the logic of bunched implications
• The semantics of BI and resource tableaux
• Undecidability of propositional separation logic and its neighbours

Cited in

(18)

• Logic for Programming, Artificial Intelligence, and Reasoning
• Separation logics and modalities: a survey
• Hypersequent and display calculi -- a unified perspective
• A labelled sequent calculus for BBI: proof theory and proof search
• Bilattice logic properly displayed
• Power and limits of structural display rules
• Reductive logic, proof-search, and coalgebra: a perspective from resource semantics
• A stone-type duality theorem for separation logic via its underlying bunched logics
• Bunched hypersequent calculi for distributive substructural logics
• Universal proof theory: semi-analytic rules and Craig interpolation
• A unified display proof theory for bunched logic
• Undecidability of propositional separation logic and its neighbours
• A complete axiomatisation for quantifier-free separation logic
• Abstract hidden Markov models: a monadic account of quantitative information flow
• The semantics and proof theory of the logic of bunched implications
• Semantical analysis of the logic of bunched implications
• Stone-type dualities for separation logics
• Displaying modal logic

Describes a project that uses

Uses Software

• jStar

This page was built for publication: Bunched logics displayed

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