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

Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/inria-00128861
Contributor : Joachim Niehren <>
Submitted on : Wednesday, March 7, 2007 - 4:16:47 PM
Last modification on : Sunday, October 27, 2019 - 1:12:02 PM
Long-term archiving on : Tuesday, April 6, 2010 - 11:08:46 PM

File

nssssMFPS23final.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00128861, version 1

Collections

Citation

Joachim Niehren, David Sabel, Manfred Schmidt-Schauß, Jan Schwinghammer. Observational Semantics for a Concurrent Lambda Calculus with Reference Cells and Futures. 23rd Conference on Mathematical Foundations of Programming Semantics, Apr 2007, New Orleans, United States. pp.313-337. ⟨inria-00128861⟩

Share

Metrics

Record views

345

Files downloads

338