headers
jcm%research.att.com | 7 Dec 1987 16:53

new address

I will begin teaching at Stanford Jan. 1, 1988.
Since I will be leaving Bell (physically) a bit
earlier to visit family, etc., all future correspondence
should be sent to the following address:

   John C. Mitchell
   Dept. of Computer Science
   Stanford University
   Stanford, CA     94305

arpa:  jcm@...

If your future travel plans call for the west
coast, please feel free to drop by.
Permalink | Reply | 0 comments |
headers
Albert R. Meyer | 9 Dec 1987 00:29
Picon

pratt@...

Date: Tue, 8 Dec 87 19:29:08 PST
From: coraki!pratt@... (Vaughan Pratt)
To: conmod@...
Subject: Wednesday seminar: Dynamic Types
Cc: friends@..., logmtc <at> sail.stanford.edu

Speaker:  Vaughan Pratt
Title:    Arithmetic of Dynamic Types
Location: MJ301
Time:     10:00-12:00, Wednesday Dec. 9

Abstract:

I will present a simplified and strengthened definition of "dynamic
type."  The basic notion of a dynamic type as an edge-labeled and
vertex-labeled graph with additional categorical structure remains
unchanged.  The difference is the elimination of the category Set from
the definition.  Besides being more in tune with modern category
theory, the new definition has the practical effect of permitting new
types to be named, the most elementary of which is 2|>2, the dynamic
type of order ideals.  Applications of 2|>2 include the definition of
the reals and the proof of Stone's theorem.  The arithmetic of order
ideals is obtained by exactly the same process as for the arithmetic of
Set = 1|>1, Cat = (1|>1)|>1, Prom = 2|>(1|>1) (whose arithmetic
constitutes the concurrent programming language SSL), etc.  I will
conclude with a discussion of the relevance of dynamic types to
Birkhoff's vision of generalized arithmetic.
-v
(Continue reading)

Permalink | Reply | 0 comments |
headers
Albert R. Meyer | 9 Dec 1987 22:42
Picon

sa@...]

From: mcvax!doc.ic.ac.uk!sa@...
Date: Mon, 7 Dec 87 17:34:20 GMT
To: meyer@...
Subject: Re:  [meyer: TYPE:TYPE]

The question of whether simulation is just Bohm tree equivalence
modified to handle weak hnf's is carefully examined by Ong in Chapter 2
of his thesis.
Surprisingly enough, he shows that it isn't.

How does bisimulation arise from non-determinism and powerdomains?
I have a clear technical answer for finitary SCCS; one gets a fully
abstract semantics (wrt bisimulation) using a domain equation
involving the Plotkin powerdomain:

  D = P[Sigma_{a in Act} D]

where Act is the action monoid, and Sigma(-) is extended separated sum
(and P is the Plotkin powerdomain with empty set).
Each iteration of the process of constructing a solution for this equation
corresponds to one level in the inductive definition of bisimulation;
the quantifier forms in the definition of bisimulation correspond to the
Egli-Milner ordering.

A detailed treatment of this and related matters is given in another draft
paper. Perhaps I should promise at this stage to send no more tantalising
hints until you have had a chance to see the details.

Best regards, Samson (Abramsky)
(Continue reading)

Permalink | Reply | 0 comments |

Gmane