The logic of bunched implications

Bulletin of Symbolic Logic 5 (2):215-244 (1999)
Abstract
We introduce a logic BI in which a multiplicative (or linear) and an additive (or intuitionistic) implication live side-by-side. The propositional version of BI arises from an analysis of the proof-theoretic relationship between conjunction and implication; it can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. The naturality of BI can be seen categorically: models of propositional BI's proofs are given by bicartesian doubly closed categories, i.e., categories which freely combine the semantics of propositional intuitionistic logic and propositional multiplicative intuitionistic linear logic. The predicate version of BI includes, in addition to standard additive quantifiers, multiplicative (or intensional) quantifiers ∀ new and ∃ new which arise from observing restrictions on structural rules on the level of terms as well as propositions. We discuss computational interpretations, based on sharing, at both the propositional and predicate levels
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/421090
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 34,938
Through your library

References found in this work BETA

On the Unity of Logic.Jean-Yves Girard - 1993 - Annals of Pure and Applied Logic 59 (3):201-217.

Add more references

Citations of this work BETA

From If to Bi.Samson Abramsky & Jouko Väänänen - 2009 - Synthese 167 (2):207 - 230.
A Comparison Between Monoidal and Substructural Logics.Clayton Peterson - 2016 - Journal of Applied Non-Classical Logics 26 (2):126-159.
Non-Normal Modalities in Variants of Linear Logic.D. Porello & N. Troquard - 2015 - Journal of Applied Non-Classical Logics 25 (3):229-255.
Why Separation Logic Works.David Pym, Jonathan M. Spring & Peter O’Hearn - forthcoming - Philosophy and Technology:1-34.

View all 10 citations / Add more citations

Similar books and articles

Analytics

Added to PP index
2009-01-28

Total downloads
13 ( #424,486 of 2,273,082 )

Recent downloads (6 months)
1 ( #376,894 of 2,273,082 )

How can I increase my downloads?

Monthly downloads

My notes

Sign in to use this feature