Concurrency and linear logic paper

Date: Wed, 2 Jan 91 23:03:40 PST

The following extended abstract can be retrieved by anonymous ftp from
boole.stanford.edu, IP address  Instructions for retrieving
this and other papers may found in /pub/README.  Contact me,
pratt@cs.stanford.edu, if you need further assistance or would prefer
to receive a copy by email.

		  Concurrent Automata and Their Logic
			   Vaughan Pratt
			Stanford University

A concurrent automaton is a poset with a top (the global initial state)
and all nonempty sups (the local initial states).  These form a
nondegenerate self-dual category Aut admitting universally definable
operations constituting a concurrent programming language and
additional operations yielding a linear logic of concurrency.  The
cofree automaton !a is a power set whose dual ?a is a free automaton by
self-duality, obtainable from !a by moving the empty set to the top.
The linear logic theory Th(CSLat) of complete semilattices strictly
extends Th(Aut), having no counterexample to !a=?a since !a and ?a are
power sets on the underlying set of a but for dual reasons.  Both
theories strictly extend linear logic with such howlers as 0=1; these
but not !a=?a are removable by intersecting with classical logic,
equivalent to taking both sides of the respective dualities as a single
model.  This makes Aut the best model of linear logic to date.  The
self-duality of both categories facilitates a noncategorical account
requiring only elementary lattice theory for a complete understanding.