Publication details
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
@TECHREPORT{NiehrenEtAl:2006:Program,
title = {Program Equivalence for a Concurrent Lambda Calculus with Futures},
author = {Joachim Niehren and David Sabel and Manfred Schmidt-Schauß and Jan Schwinghammer},
year = {2006},
month = {Oct},
number = {Frank-26},
address = {Fachbereich Informatik und Mathematik},
institution = {J.W.Goethe Universität Frankfurt},
note = {Revised version appeared Proc. of Mathematical Foundations of Programming Semantics (23rd MFPS), April 2007},
}
Login to edit
Legal notice, Privacy policy
