Copenhagen Programming Language Seminar

A Concurrent Lambda Calculus with Futures

Jan Schwinghammer
Saarland University

Monday 9 March 2009, 14:00-15:00
The IT University, Rued Langgaards Vej 7, DK-2300 Auditorium 3


Alice ML is an extension of Standard ML with shared-memory concurrency and a form of data-driven synchronization based on futures. A future is a transparent placeholder for a value, which is either assigned explicitly, or obtained as the result of a concurrent computation. Higher-level concurrency constructs like buffers and channels can be implemented in terms of futures.

I will present a lambda calculus with futures and ML-style general references that models the concurrent core of Alice ML. The calculus is equipped with a small-step operational semantics, which induces a contextual equivalence based on the may- and must-convergence behaviour of programs. In order to reason about the correctness of an implementation of buffers, a context lemma and a number of program transformations are proved correct using diagram-based methods.

Scientific host:Lars Birkedal Administrative host: Annette Enggaard. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org