We, Peter O'Hearn and David Pym, are pleased to announce our new paper, ``The Logic of Bunched Implications''. We hope it will be of interest to readers of `categories'. BI is a relevant logic which extends both linear and intuitionistic logic. It has a semantics of proofs based on `doubly closed categories', which carry two monoidal closed structures, one of which is cartesian in models of BI. A rich class of models is provided by Day's tensor product construction on the category of presheaves over a small monoidal category. It also comes with a lambda calculus, a truth semantics and a computational interpretation as a logic of resources, quite different from that of linear logic. The paper is available at: http://www.dcs.qmw.ac.uk/~pym and http://www.dcs.qmw.ac.uk/~ohearn where drafts of various companion and related papers can/will be found. P.W.O'Hearn and D.J. Pym Queen Mary & Wesfield College, University of London Abstract. 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, and may be viewed as a merging of intuitionistic logic and multiplicative, intuitionistic linear logic. The predicate version of BI includes, in addition to standard additive quantifiers, multiplicative (or intensional) quantifiers ``forall-new'' and ``exist-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.
participants (1)
-
David J. Pym