Publication details

Saarland University Computer Science

Program Equivalence for a Concurrent Lambda Calculus with Futures

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

Technical Report, J.W.Goethe Universität Frankfurt, Fachbereich Informatik und Mathematik, Revised version appeared Proc. of Mathematical Foundations of Programming Semantics (23rd MFPS), April 2007, October 2006

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

Legal notice, Privacy policy