HAL - INRIA :: [inria-00128861, version 1] Observational Semantics for a Concurrent Lambda Calculus with Reference Cells and Futures

inria-00128861, version 1

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 173 (2007) 313-337

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.

1: MOSTRARE (INRIA Futurs)
INRIA – CNRS : UMR8022 – Université des Sciences et Technologies de Lille - Lille I : EA3588 – Université Charles de Gaulle - Lille III
2: J. W. Goethe-Universität
J. W. Goethe-Universitat – Goethe Universität
3: Programming Systems Lab [Saarland]
Saarland University

inria-00128861, version 1
http://hal.inria.fr/inria-00128861
oai:hal.inria.fr:inria-00128861
From: Joachim Niehren <>
Submitted on: Wednesday, 7 March 2007 16:16:47
Updated on: Monday, 14 December 2009 22:24:30

See detailed view

Associated documents

PDF :

Export

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Peer-reviewed conferences/proceedings</head>
<biblStruct type="inproceedings" xml:id="inria-00128861"><analytic>
<author><persName><forename>Joachim</forename><surname>Niehren</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Futurs</orgName>
<orgName type="team">MOSTRARE</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR8022</orgName>
<orgName type="institution">Université des Sciences et Technologies de Lille - Lille I : EA3588</orgName>
<orgName type="institution">Université Charles de Gaulle - Lille III</orgName>
</affiliation>
</author>
<author><persName><forename>David</forename><surname>Sabel</surname></persName>
<affiliation>
<orgName type="team">J. W. Goethe-Universität</orgName>
<country>DE</country>
<orgName type="institution">J. W. Goethe-Universitat</orgName>
<orgName type="institution">Goethe Universität</orgName>
</affiliation>
</author>
<author><persName><forename>Manfred</forename><surname>Schmidt-Schauß</surname></persName>
<affiliation>
<orgName type="team">J. W. Goethe-Universität</orgName>
<country>DE</country>
<orgName type="institution">J. W. Goethe-Universitat</orgName>
<orgName type="institution">Goethe Universität</orgName>
</affiliation>
</author>
<author><persName><forename>Jan</forename><surname>Schwinghammer</surname></persName>
<affiliation>
<orgName type="team">Programming Systems Lab [Saarland]</orgName>
<country>DE</country>
<orgName type="institution">Saarland University</orgName>
</affiliation>
</author>
<title type="main" level="a">Observational Semantics for a Concurrent Lambda Calculus with Reference Cells and Futures</title></analytic><monogr><meeting>23rd Conference on Mathematical Foundations of Programming Semantics</meeting><imprint><pubPlace><settlement>New Orleans</settlement><country>United States</country></pubPlace><biblScope type="publicationDate">2007-04-11</biblScope><biblScope type="vol">173</biblScope><biblScope type="pp">313-337</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/inria-00128861</idno><idno type="HALFile">http://hal.inria.fr/inria-00128861/PDF/nssssMFPS23final.pdf</idno></biblStruct>
</listBibl>
</listBibl>