The Logic of Events and Event Structure Patterns
An event structure is an abstract model of an execution of a distributed
system. It contains all the information usually represented in a
"message sequence diagram" and from its primitives we may
define Lamport's causal ordering of events.
The Logic of Events is a constructive logic where the propositions
are about event structures and the realizers of these propositions
are abstract distributed programs, called distributed message automata.
The definition of this logic in Nuprl is now fairly elegant --
there are six axioms for event structures and nine rules for realizing
In the first part of the seminar, I will go over the logic and
present a simple example of deriving a program from a specification.
In the second part, I will discuss a newer result.
We have defined a class of expressions, reminiscent of regular
called ESP (event structure patterns), and given them a precise meaning
as event structure propositions. Every ESP expression is realizable
(this is the new resut) and so they form a new set of compoonents
for building distributed systems.