[Prev][Next][Index][Thread]

Recent papers relevant to linear logic



The following papers treat properties of Chu spaces and their
applications to foundations and concurrency modelling.  They may be
retrieved by anonymous ftp from boole.stanford.edu:/pub.  See also the
file ABSTRACTS in that directory for these and other papers.

Chu spaces are relevant to linear logic as the natural logic of the Chu
construction, as observed by Barr during Girard's talk at the 1987
Boulder conference "Categories in CS and Logic."  Chu spaces over K
(also called "games over K" by Lafont and Streicher [LICS'91, 43-49],
"Chu space" was proposed by Barr in email correspondence) are the
objects of the category Chu(Set,K), Chu's construction applied to Set
(as a symmetric monoidal closed category) with dualizer the set K.

Vaughan Pratt

=======================

scbr.tex

        @InProceedings(
Pr93b,  Author="Pratt, V.R.",
        Title="The Second Calculus of Binary Relations",
        Booktitle="MFCS'93, Gda{\'{n}}sk", Address="Poland", Year=1993)

We view the Chu space interpretation of linear logic as an alternative
interpretation of the language of the Peirce calculus of binary
relations.  Chu spaces amount to K-valued binary relations, which for
K=2^n we show generalize n-ary relational structures.  We also exhibit
a four-stage unique factorization system for Chu transforms that
illuminates their operation.

=======================

gates.tex

        @InProceedings(
GP93,   Author="Gupta, V. and Pratt, V.R.",
        Title="Gates Accept Concurrent Behavior",
        Booktitle="Proc. 34th Ann. IEEE Symp. on Foundations of Comp. Sci.",
	Pages="62-71", Month=Nov, Year=1993)

We represent concurrent processes as Boolean propositions or gates,
cast in the role of acceptors of concurrent behavior.  This properly
extends other mainstream representations of concurrent behavior such as
event structures, yet is defined more simply.  It admits an intrinsic
notion of duality that permits processes to be viewed as either
schedules or automata.  Its algebraic structure is essentially that of
linear logic, with its morphisms being consequence-preserving renamings
of propositions, and with its operations forming the core of a natural
concurrent programming language.

=======================

cks.tex

	@InProceedings(
Gup93,  Author="Gupta, V.",
	Title="Concurrent Kripke Structures",
	Booktitle="Proceedings of the North American Process Algebra
	Workshop, Cornell CS-TR-93-1369", Month=Aug, Year=1993)

We consider a class of Kripke Structures in which the atomic
propositions are events.  This enables us to represent worlds as sets
of events and the transition and satisfaction relations of Kripke
structures as the subset and membership relations on sets.  We use this
class, called event Kripke structures, to model concurrency.  The
obvious semantics for these structures is a true concurrency
semantics.  We show how several aspects of concurrency can be easily
defined, and in addition get distinctions between causality and
enabling, and choice and nondeterminism.  We define a duality for event
Kripke structures, and show how this duality enables us to convert
between imperative and declarative views of programs, by treating
states and events on the same footing.  We provide pictorial
representations of both these views, each encoding all the information
to convert to the other.

We define a process algebra of event Kripke structures, showing how to
combine them in the usual ways---parallel composition, sequential
composition, choice, interaction and iteration.  Various properties of
these connectives like associativity and distributivity are proved.  We
then show that Winskel's event structures can be embedded in the class
of event Kripke structures, and define partial synchronous composition,
the primary connective for event structures, for event Kripke
structures, and show its equivalence to Winskel's definition.