Thu Jan 8, 2008, 4:15-5:30, 3400 Boelter Hall

A Model of Cooperative Threads

Gordon Plotkin
University of Edinburgh

We develop a model of concurrent imperative programming with threads. We
focus on a small imperative language with cooperative threads which execute
without interruption until they terminate or explicitly yield control.  We
define and study a trace-based denotational semantics for this language;
this semantics is fully abstract but mathematically elementary.  We also
give an equational theory for the computational effects that underlie the
language, including thread spawning.  We then analyze threads in terms of
the free algebra monad for this theory.

About the speaker:  Gordon Plotkin is a Professor of Computer Science
at the University of Edinburgh, Scotland.  Plotkin received his PhD in 1972 
from the University of Edinburgh, advised by Rod Burstall.  Plotkin is a 
Fellow of the Royal Society and a member of Academia Europaea, 
the European Academy of Science.  In 1981 Plotkin introduced 
Structural Operational Semantics, a technique for describing the 
formal semantics of programs.  Since the early 1990s, 
Structural Operational Semantics took over and became the dominant style 
of writing semantics of programming languages.  The paper on 
Structural Operational Semantics was a technical report from 
University of Aarhus, Denmark, and has received more than 2,000 citations 
on Google Scholar.  Among many other widely cited and hugely influential 
papers are "LCF considered as a programming language", "call-by-name,
call-by-value, and lambda calculus", powerdomains, ideal models,
and abstract types have existential types.  Plotkin has graduated 
many PhD students, including several who have gone on to become 
stars of Computer Science, including Luca Cardelli, Eugenio Moggi, 
and Glynn Winskel.

Hosts: Eli Gafni and Jens Palsberg