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.
Type de document :
Communication dans un congrès
23rd Conference on Mathematical Foundations of Programming Semantics, Apr 2007, New Orleans, United States. 173, pp.313-337, 2007, Electronic Notes in Theoretical Computer Science
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00128861
Contributeur : Joachim Niehren <>
Soumis le : mercredi 7 mars 2007 - 16:16:47
Dernière modification le : jeudi 11 janvier 2018 - 06:22:13
Document(s) archivé(s) le : mardi 6 avril 2010 - 23:08:46

Fichier

nssssMFPS23final.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. 173, pp.313-337, 2007, Electronic Notes in Theoretical Computer Science. 〈inria-00128861〉

Partager

Métriques

Consultations de la notice

276

Téléchargements de fichiers

179