Publication details

Saarland University Computer Science

Observational Semantics for a Concurrent Lambda Calculus with Reference Cells and Futures

Joachim Niehren, David Sabel, Manfred Schmidt-Schauß, Jan Schwinghammer

23rd Conference on Mathematical Foundations of Programming Semantics (MFPS XXIII), April 2007


We present an observational semantics for lambda(fut), a concurrent lambda calculus with reference cells and futures. The calculus lambda(fut) models the operational semantics of the concurrent higher-order programming language Alice ML. Our result is a powerful notion of equivalence that is the coarsest nontrivial congruence distinguishing observably different processes. It justifies a maximal set of correct program transformations, and it includes all of lambda(fut)'s deterministic reduction rules, in particular, call-by-value beta reduction.

Based on earlier technical report TR Frank-26

Download PDF        Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009