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

We present an observational semantics for λ(fut), a concurrent λ-calculus with reference cells and futures. The calculus λ(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 λ(fut)'s deterministic reduction rules, in particular, call-by-value β-reduction.