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
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.
show moreshow less

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
URL:http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank-26.pdf
Parent Title (English):Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 26
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
Year of Completion:2006
Year of first Publication:2006
Publishing Institution:Univ.-Bibliothek Frankfurt am Main
Release Date:2006/10/30
Tag:Alice ML ; Contextual Equivalence; Futures; Lambda Calculus ; Operational Semantics
SWD-Keyword:Lambda-Kalkül; ML <Programmiersprache> ; Nebenläufigkeit; Operationale Semantik
Pagenumber:28
First Page:1
Last Page:28
Institutes:Informatik
Dewey Decimal Classification:004 Datenverarbeitung; Informatik
Sammlungen:Universitätspublikationen
Licence (German):License Logo Veröffentlichungsvertrag für Publikationen

$Rev: 11761 $