{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T02:06:41Z","timestamp":1781143601725,"version":"3.54.1"},"reference-count":44,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,1,15]],"date-time":"2014-01-15T00:00:00Z","timestamp":1389744000000},"content-version":"unspecified","delay-in-days":5342,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Bull. symb. log."],"published-print":{"date-parts":[[1999,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We introduce a logic<jats:bold>BI<\/jats:bold>in which a multiplicative (or linear) and an additive (or intuitionistic) implication live side-by-side. The propositional version of<jats:bold>BI<\/jats:bold>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<jats:bold>BI<\/jats:bold>can be seen categorically: models of propositional<jats:bold>BI'<\/jats:bold>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<jats:bold>BI<\/jats:bold>includes, in addition to standard additive quantifiers, multiplicative (or intensional) quantifiers<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S1079898600007022_inline1\"\/>and<jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S1079898600007022_inline2\"\/>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.<\/jats:p>","DOI":"10.2307\/421090","type":"journal-article","created":{"date-parts":[[2006,5,7]],"date-time":"2006-05-07T07:12:41Z","timestamp":1146985961000},"page":"215-244","source":"Crossref","is-referenced-by-count":319,"title":["The Logic of Bunched Implications"],"prefix":"10.1017","volume":"5","author":[{"given":"Peter W.","family":"O'Hearn","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David J.","family":"Pym","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,1,15]]},"reference":[{"key":"S1079898600007022_ref019","unstructured":"Ishtiaq S. S. and Pym D. J. , Kripke resource models of a dependently-typed, bunched \u03bb-calculus, in preparation, available at http:\/\/www.dcs.qmw.ac.uk\/~pym."},{"key":"S1079898600007022_ref001","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90181-R"},{"key":"S1079898600007022_ref041","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569807.016"},{"key":"S1079898600007022_ref014","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-5203-4_3"},{"key":"S1079898600007022_ref020","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/8.6.809"},{"key":"S1079898600007022_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0063099"},{"key":"S1079898600007022_ref027","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90068-W"},{"key":"S1079898600007022_ref043","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1093\/oso\/9780198537779.003.0013","volume-title":"Substructural logics","author":"Troelstra","year":"1993"},{"key":"S1079898600007022_ref016","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(93)90093-S"},{"key":"S1079898600007022_ref023","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90100-4"},{"key":"S1079898600007022_ref021","volume-title":"Mathematical logic","author":"Kleene","year":"1968"},{"key":"S1079898600007022_ref008","volume-title":"Proceedings of computer science logic '94, Kazimierz, Poland","author":"Benton","year":"1995"},{"key":"S1079898600007022_ref006","doi-asserted-by":"publisher","DOI":"10.1007\/BF00284976"},{"key":"S1079898600007022_ref042","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/092\/1003210"},{"key":"S1079898600007022_ref038","first-page":"345","volume-title":"Algorithmic languages: Proceedings of the international symposium on algorithmic languages","author":"Reynolds","year":"1981"},{"key":"S1079898600007022_ref035","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/4.2.175"},{"key":"S1079898600007022_ref034","unstructured":"Pym D. J. , The semantics and proof theory of the logic of bunched implications, I: Propositional BI, available on the web at http:\/\/www.dcs.qmw.ac.uk\/~pym, 1998."},{"key":"S1079898600007022_ref018","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1036"},{"key":"S1079898600007022_ref039","volume-title":"Proceedings of CSL '97","author":"Ruet","year":"1997"},{"key":"S1079898600007022_ref022","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71685-9"},{"key":"S1079898600007022_ref026","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(89)90031-9"},{"key":"S1079898600007022_ref036","volume-title":"Relevant logic: a philosophical examination of inference","author":"Read","year":"1987"},{"key":"S1079898600007022_ref004","volume-title":"Entailment: the logic of relevance and necessity","volume":"II","author":"Anderson","year":"1992"},{"key":"S1079898600007022_ref029","volume-title":"Theoretical Computer Science","author":"O'Hearn"},{"key":"S1079898600007022_ref030","volume-title":"Algol-like languages","volume":"two","author":"O'Hearn","year":"1997"},{"key":"S1079898600007022_ref033","unstructured":"Pym D. J. , The semantics and proof theory of the logic of bunched implications, II: predicate BI, available on the web at http:\/\/www.dcs.qmw.ac.uk\/~pym, 1998."},{"key":"S1079898600007022_ref024","volume-title":"Introduction to higher-order categorical logic","author":"Lambek","year":"1986"},{"key":"S1079898600007022_ref031","unstructured":"Plotkin G. D. , Type theory and recursion, slides for Scottfest talk, 1993."},{"key":"S1079898600007022_ref040","volume-title":"A structure for plans and behaviour","author":"Sacerdoti","year":"1977"},{"key":"S1079898600007022_ref015","first-page":"1","volume-title":"Theoretical Computer Science","author":"Girard","year":"1987"},{"key":"S1079898600007022_ref013","unstructured":"Dunn J. M. , Conseqution formulation of positive R with co-tenability and t, in [3]."},{"key":"S1079898600007022_ref037","first-page":"39","volume-title":"Conference record of the fifth annual acm symposium on principles of programming languages","author":"Reynolds","year":"1978"},{"key":"S1079898600007022_ref010","first-page":"1","volume-title":"Reports of the midwest category seminar","author":"Day","year":"1970"},{"key":"S1079898600007022_ref025","volume-title":"Technical Report 2","author":"Martin-L\u00f6f","year":"1982"},{"key":"S1079898600007022_ref005","unstructured":"Barber A. and Plotkin G. D. , Dual intuitionistic linear logic, submitted, 10 1997."},{"key":"S1079898600007022_ref028","volume-title":"Typed \u03bb-calculus and applications","author":"O'Hearn","year":"1999"},{"key":"S1079898600007022_ref044","first-page":"1059","volume":"49","author":"Urquhart","year":"1972","journal-title":"Semantics for relevant logics"},{"key":"S1079898600007022_ref002","unstructured":"Ambler S. , First order linear logic in symmetric monoidal closed categories, Ph.D. thesis , University of Edinburgh, 1992."},{"key":"S1079898600007022_ref032","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)01183-7"},{"key":"S1079898600007022_ref007","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1093\/oso\/9780198537779.003.0002","volume-title":"Substructural logics","author":"Belnap","year":"1993"},{"key":"S1079898600007022_ref003","volume-title":"Entailment: the logic of relevance and necessity, volume I","author":"Anderson","year":"1975"},{"key":"S1079898600007022_ref017","first-page":"391","volume-title":"Proceedings of AMAST '96","author":"Harland","year":"1996"},{"key":"S1079898600007022_ref012","first-page":"1","volume-title":"Substructural logics","author":"Do\u0161sen","year":"1993"},{"key":"S1079898600007022_ref009","volume-title":"Mathematical foundations of programming semantics, eleventh annual conference","author":"Brookes","year":"1995"}],"container-title":["Bulletin of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1079898600007022","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,4]],"date-time":"2024-02-04T07:36:33Z","timestamp":1707032193000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1079898600007022\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,6]]},"references-count":44,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1999,6]]}},"alternative-id":["S1079898600007022"],"URL":"https:\/\/doi.org\/10.2307\/421090","relation":{},"ISSN":["1079-8986","1943-5894"],"issn-type":[{"value":"1079-8986","type":"print"},{"value":"1943-5894","type":"electronic"}],"subject":[],"published":{"date-parts":[[1999,6]]}}}