Typing for Concurrent Systems

Peter Sewell

(University of Cambridge)

Typing for sequential languages is reasonably well understood. In contrast, types that capture behavioural disciplines of concurrent systems are only beginning to be intensively studied. In this talk I'll give a non-technical overview of some recent work in the area, illustrating the range of possible motivations and results.

I'll touch on type systems for variants of the pi-calculus that prevent run-time errors (via simple typing), support operational reasoning and guarantee confluence (via input/output subtyping and linear typing), and allow implementation optimisations in a distributed setting (via located channel subtyping). I'll conclude by briefly discussing type systems for synchronous circuits that support compositional abstraction results.
Tuesday 29th April 1997, 14:30
Seminar Room 322
Department of Computer Science