Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik
1 search hit
- 26
-
Program Equivalence for a Concurrent Lambda Calculus with Futures
(2006)
-
Joachim Niehren
David Sabel
Manfred Schmidt-Schauß
Jan Schwinghammer
- 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 Lambda(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 Lambda(fut). This relies on a number of fundamental properties that we establish for our observational semantics.
