Observational Semantics for a Concurrent Lambda Calculus with Reference Cells and Futures - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2007

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

Résumé

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.
Fichier principal
Vignette du fichier
nssssMFPS23final.pdf (334.74 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00128861 , version 1 (07-03-2007)

Identifiants

  • HAL Id : inria-00128861 , version 1

Citer

Joachim Niehren, David Sabel, Manfred Schmidt-Schauss, 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⟩
144 Consultations
186 Téléchargements

Partager

Gmail Facebook X LinkedIn More