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 Lam(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 Lam(fut). This relies on a number of fundamental properties that we establish for our observational semantics.
Download PDF Show BibTeX
Login to edit