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

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Joachim Niehren, David SabelORCiDGND, Manfred Schmidt-SchaußORCiDGND, 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:Universitätsbibliothek Johann Christian Senckenberg
Release Date:2006/10/30
Tag:Alice ML; Contextual Equivalence; Futures; Lambda Calculus; Operational Semantics
GND Keyword:Lambda-Kalkül; ML <Programmiersprache>; Operationale Semantik; Nebenläufigkeit
Page Number:28
First Page:1
Last Page:28
HeBIS-PPN:344372464
Institutes:Informatik und Mathematik / Informatik
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Licence (German):License LogoDeutsches Urheberrecht