Skip to Main content Skip to Navigation
Journal articles

A Concurrent Lambda Calculus with Futures

Joachim Niehren 1 Jan Schwinghammer 2 Gert Smolka 2 
1 MOSTRARE - Modeling Tree Structures, Machine Learning, and Information Extraction
LIFL - Laboratoire d'Informatique Fondamentale de Lille, Inria Lille - Nord Europe
Abstract : We introduce a new lambda calculus with futures, Lambda(fut), that models the operational semantics of concurrent statically typed functional programming languages with mixed eager and lazy threads such as Alice ML, a concurrent extension of Standard ML. Lambda(fut) is a minimalist extension of the call-by-value lambda-calculus that is sufficiently expressive to define and combine a variety of standard concurrency abstractions, such as channels, semaphores, and ports. Despite its minimality, the basic machinery of Lambda(fut) is sufficiently powerful to support explicit recursion and call-by-need evaluation. We present a static type system for Lambda(fut) and distinguish a fragment of Lambda(fut) that we prove to be uniformly confluent. This result confirms our intuition that reference cells are the sole source of indeterminism. This fragment assumes the absence of so called {handle errors} that violate the single assignment assumption of Lambda(fut)'s handled future-construct. Finally, we present a linear type system for Lambda(fut) by which to prove the absence of handle errors. Our system is rich enough to type definitions of the above mentioned concurrency abstractions. Consequently, these cannot be corrupted in any (not necessarily linearly) well-typed context.
Document type :
Journal articles
Complete list of metadata

Cited literature [38 references]  Display  Hide  Download
Contributor : Joachim Niehren Connect in order to contact the contributor
Submitted on : Thursday, August 31, 2006 - 6:52:58 PM
Last modification on : Friday, February 4, 2022 - 3:17:40 AM
Long-term archiving on: : Monday, September 20, 2010 - 4:51:43 PM





Joachim Niehren, Jan Schwinghammer, Gert Smolka. A Concurrent Lambda Calculus with Futures. Theoretical Computer Science, Elsevier, 2006, Theoretical Computer Science, 364 (3), pp.338-356. ⟨10.1016/j.tcs.2006:08.016⟩. ⟨inria-00090434v2⟩



Record views


Files downloads