[Prev][Next][Index][Thread]
Re: Non-commutative linear logic
-
To: types
-
Subject: Re: Non-commutative linear logic
-
From: ma@src.dec.com (Martin Abadi)
-
Date: Thu, 06 Feb 92 10:40:01 EST
-
In-Reply-To: Message of Wed, 05 Feb 92 11:05:23 EST from Mike Dunn <dunn@iuvax.cs.indiana.edu> <199202051605.AA02707@stork.lcs.mit.edu>
-
Sender: meyer@theory.lcs.mit.edu
Date: Wed, 5 Feb 92 11:47:08 PST
Cc: Mike Dunn <dunn@iuvax.cs.indiana.edu>
In fact, the model that Gordon Plotkin and I defined (POPL 91) and
that Vaughan mentioned recently has a distributive-lattice part.
And there is a concrete operation # corresponding to the Routley's
*, just explained by Mike Dunn: if M is a fact, a transition sequence
u (a sequence of pairs of states) satisfies M iff u# does not satisfy
M^\perp, where u# is the "least" transition sequence that "crashes"
with u.
Martin Abadi