Theory Seminar, P.Sewell, 97 06 27 
Theory Seminar


On Implementations and Semantics 
of a Concurrent Programming Language

Peter Sewell, University of Cambridge
Friday 27 June 1997 at 2pm in TP4

The concurrency theory literature contains many proposals for models of process algebras. In this work I consider an example application of the pi-calculus, the programming language Pict of Pierce and Turner, primarily in order to see how far it is possible to argue, from facts about the application, that some model is the most appropriate.

I will discuss informally the sense in which the semantics of Pict relates to the behaviour of actual implementations. An operational model can be given, reflecting this discussion, of the interactions between a Pict implementation (considered as the abstract behaviour of a C program) and its environment (modelling an operating system and user). This leads to definitions of a class of abstract machines and abstract machine correctness, using an adapted notion of testing, and to a proof that a sample abstract machine is indeed correct. I will then briefly discuss the standard of correctness appropriate for program transformations and the induced precongruence.

Many of the semantic choices do indeed turn out to be determined by facts about Pict; some points should be applicable to other nondeterministic programming languages.

(This is a copy of a talk to be given at CONCUR, so it should be short - only 25 minutes or so.)