Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

Observational Semantics for a Concurrent Lambda Calculus with Reference Cells and Futures

Joachim Niehren, David Sabel, Manfred Schmidt-Schauß, Jan Schwinghammer

23rd Conference on Mathematical Foundations of Programming Semantics (MFPS XXIII), April 2007

We present an observational semantics for lambda(fut), a concurrent lambda calculus with reference cells and futures. The calculus lambda(fut) models the operational semantics of the concurrent higher-order programming language Alice ML. Our result is a powerful notion of equivalence that is the coarsest nontrivial congruence distinguishing observably different processes. It justifies a maximal set of correct program transformations, and it includes all of lambda(fut)'s deterministic reduction rules, in particular, call-by-value beta reduction.

Based on earlier technical report TR Frank-26

Download PDF        Show BibTeX               

@INPROCEEDINGS{NiehrenEtAl:2007:Observational,
  title = {Observational Semantics for a Concurrent Lambda Calculus with Reference Cells and Futures},
  author = {Joachim Niehren and David Sabel and Manfred Schmidt-Schauß and Jan Schwinghammer},
  year = {2007},
  month = {Apr},
  booktitle = {23rd Conference on Mathematical Foundations of Programming Semantics (MFPS XXIII)},
  series = {{ENTCS}},
  address = {{New Orleans}},
  note = {{Accepted}},
}

Login to edit