A Concurrent Lambda Calculus with Futures

Reasoning about the correctness of program transformations requires a notion of program equivalence. We present an observational semantics for the concurrent lambda calculus with futures λ(fut), which formalizes the operational semantics of the programming language Alice ML. We show that natural program optimizations, as well as partial evaluation with respect to deterministic rules, are correct for λ(fut). This relies on a number of fundamental properties that we establish for our observational semantics.

• Type: Conference
• Year: 2005
• Where: FROCOS
• Authors: Joachim Niehren, Jan Schwinghammer, Gert Smolka
• Keywords: Concurrent Lambda Calculus, FROCOS 2005, Language Alice Ml, Observational Semantics