The Logic of Bunched Implications

DOI10.2307/421090zbMath0930.03095DBLPjournals/bsl/OHearnP99OpenAlexW2008132476WikidataQ56445140 ScholiaQ56445140MaRDI QIDQ4262604

Peter W. O'Hearn, David J. Pym

Publication date: 22 September 1999

Published in: Bulletin of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: http://www.math.ucla.edu/~asl/bsl/0502-toc.htm

zbMATH Keywords

multiplicative quantifiers computational interpretations bi-Cartesian doubly closed categories merging of intuitionistic logic and multiplicative intuitionistic linear logic proof-theoretic relationship between conjunction and implication restrictions on structural rules

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (only showing first 100 items - show all)

An algebraic glimpse at bunched implications and separation logic ⋮ Bunched sequential information ⋮ Convolution as a Unifying Concept ⋮ Program Verification with Separation Logic ⋮ Completeness of Nominal PROPs ⋮ A spatial logic for concurrency. II ⋮ A stone-type duality theorem for separation logic via its underlying bunched logics ⋮ AFFINE LOGIC FOR CONSTRUCTIVE MATHEMATICS ⋮ From IF to BI. A tale of dependence and separation ⋮ Uniqueness logic ⋮ Linear and affine logics with temporal, spatial and epistemic operators ⋮ A logic of separating modalities ⋮ Model checking mobile ambients ⋮ A spatial logic for concurrency. I ⋮ Developments in concurrent Kleene algebra ⋮ Automated Theorem Proving for Assertions in Separation Logic with All Connectives ⋮ Bringing Order to the Separation Logic Jungle ⋮ A Unified Display Proof Theory for Bunched Logic ⋮ An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics ⋮ A Modal BI Logic for Dynamic Resource Properties ⋮ Completeness for a First-Order Abstract Separation Logic ⋮ A perspective on specifying and verifying concurrent modules ⋮ A calculus and logic of resources and processes ⋮ The Lambek calculus extended with intuitionistic propositional logic ⋮ Undecidability of Propositional Separation Logic and Its Neighbours ⋮ Abstract categorical semantics for resourceful functional reactive programming ⋮ Separation logic and logics with team semantics ⋮ A semantics for concurrent separation logic ⋮ Resources, concurrency, and local reasoning ⋮ Relational separation logic ⋮ A Program Construction and Verification Tool for Separation Logic ⋮ Coalgebraic completeness-via-canonicity for distributive substructural logics ⋮ Temporal BI: proof system, semantics and translations ⋮ Inter-process buffers in separation logic with rely-guarantee ⋮ Separation logics and modalities: a survey ⋮ Non-normal modalities in variants of linear logic ⋮ A comparison between monoidal and substructural logics ⋮ Adjunct Elimination in Context Logic for Trees ⋮ Proof tactics for assertions in separation logic ⋮ Bunched logics displayed ⋮ Lewis meets Brouwer: constructive strict implication ⋮ Semantical analysis of the logic of bunched implications ⋮ An epistemic separation logic with action models ⋮ A System of Interaction and Structure III: The Complexity of BV and Pomset Logic ⋮ Varieties of unary-determined distributive $\ell$-magmas and bunched implication algebras ⋮ A framework for substructural type systems ⋮ Unnamed Item ⋮ A calculus and logic of bunched resources and processes ⋮ Unary-determined distributive $\ell $-magmas and bunched implication algebras ⋮ Some modal and temporal translations of generalized basic logic ⋮ Expressing second-order sentences in intuitionistic dependence logic ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic ⋮ The Essence of Higher-Order Concurrent Separation Logic ⋮ Bunched polymorphism ⋮ Focused proof-search in the logic of bunched implications ⋮ Footprints in Local Reasoning ⋮ A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language ⋮ The virtues of idleness: a decidable fragment of resource agent logic ⋮ Unnamed Item ⋮ Two-dimensional linear algebra ⋮ Pseudo-commutative Monads ⋮ Separation Logic Semantics for Communicating Processes ⋮ Maude as a Platform for Designing and Implementing Deep Inference Systems ⋮ Counting the Cost in the Picalculus (Extended Abstract) ⋮ Preface to the special volume ⋮ Adjunct elimination in context logic for trees ⋮ Join-completions of partially ordered algebras ⋮ Algebra and logic for access control ⋮ Normal proofs, cut free derivations and structural rules ⋮ Disjunction property and complexity of substructural logics ⋮ A coordination approach to mobile components ⋮ Unnamed Item ⋮ Matching Logic: An Alternative to Hoare/Floyd Logic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning ⋮ On Temporal and Separation Logics ⋮ An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning ⋮ Unnamed Item ⋮ Intuitionistic Layered Graph Logic ⋮ A Substructural Epistemic Resource Logic ⋮ Completeness and Herbrand theorems for nominal logic ⋮ Truth-values as labels: a general recipe for labelled deduction ⋮ Algebra and logic for resource-based systems modelling ⋮ On Model Checking Boolean BI ⋮ Nested Hoare Triples and Frame Rules for Higher-Order Store ⋮ Term Sequent Logic ⋮ Fine-grained concurrency with separation logic ⋮ Possible worlds and resources: The semantics of $\mathbf{BI}$ ⋮ An adaptation-complete proof system for local reasoning about cloud storage systems ⋮ Proof-search in type-theoretic languages: An introduction ⋮ Separation Logic Tutorial ⋮ Separation Logic Contracts for a Java-Like Language with Fork/Join ⋮ Unnamed Item ⋮ Local Reasoning about Data Update ⋮ Manipulating Trees with Hidden Labels ⋮ Systems Modelling via Resources and Processes: Philosophy, Calculus, Semantics, and Logic ⋮ Decision problems in a logic for reasoning about reconfigurable distributed systems ⋮ Hybridizing a Logical Framework ⋮ On the relation between concurrent separation logic and concurrent Kleene algebra

Cites Work

This page was built for publication: The Logic of Bunched Implications