From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/843 Path: news.gmane.org!not-for-mail From: "David J. Pym" Newsgroups: gmane.science.mathematics.categories Subject: The Logic of Bunched Implications. Date: Mon, 03 Aug 1998 14:18:11 +0100 Organization: Queen Mary & Westfield College, University of London Message-ID: <35C5B893.ABD78F49@dcs.qmw.ac.uk> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241017229 27790 80.91.229.2 (29 Apr 2009 15:00:29 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:00:29 +0000 (UTC) Cc: pym@dcs.qmw.ac.uk, ohearn@dcs.qmw.ac.uk To: categories@mta.ca Original-X-From: cat-dist Mon Aug 3 17:58:16 1998 Original-Received: (from Majordom@localhost) by mailserv.mta.ca (8.8.8/8.8.8) id QAA11495 for categories-list; Mon, 3 Aug 1998 16:07:06 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Mailer: Mozilla 4.04 [en] (X11; I; Linux 2.0.30 i586) Original-Sender: cat-dist@mta.ca Precedence: bulk Original-Lines: 51 Xref: news.gmane.org gmane.science.mathematics.categories:843 Archived-At: 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.