Talk by Laura Bocchi, University of Kent
BACKGROUND:
Type checking helps prevent runtime errors by statically verifying that program entities are used according to their types. A common example is checking that variables match their declared data types. But types can describe more than just values: session types, for instance, capture communication patterns involving message-passing send/receive actions. These can be thought of as application-level protocols that distributed programs are expected to follow.
In this tutorial, I will give a gentle introduction to asynchronous session types, their key properties, and their notion of subtyping. Starting from a safe system, session subtyping lets you replace a process of type T with another of type T′—with a different communication behaviour—without compromising safety.
Although asynchronous session subtyping is undecidable in general, we can rely on practical approximate algorithms. I will briefly show a recent algorithm, based on the idea of applying abstract interpretation to communication structures, which has given encouraging results.
PREPARATION:
Additional materials may be circulated nearer the day.
SPEAKER:
by