Program Equivalence for 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 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.

Download full text files

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

    Share in Twitter Search Google Scholar
Metadaten
Author:Joachim Niehren, David Sabel, Manfred Schmidt-Schauß, Jan Schwinghammer
URN:urn:nbn:de:hebis:30-32230
Series (Serial Number)Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik (26)
Publisher:Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology
Place of publication:Frankfurt [am Main]
Document Type:Working Paper
Language:English
Date of Publication (online):30.10.2006
Year of first Publication:2006
Publishing Institution:Univ.-Bibliothek Frankfurt am Main
Tag:Alice ML ; Contextual Equivalence; Futures; Lambda Calculus ; Operational Semantics
SWD-Keyword:Lambda-Kalkül; ML <Programmiersprache> ; Nebenläufigkeit; Operationale Semantik
Source:Technical Report Frank 26, Institut für Informatik, Johann Wolfgang Goethe-Universität Frankfurt am Main
Institutes:Informatik
Dewey Decimal Classification:004 Datenverarbeitung; Informatik
Sammlungen:Universitätspublikationen
Licence (German):License Logo Veröffentlichungsvertrag für Publikationen ohne Print on Demand

OPUS4 Logo

$Rev: 8725 $