# zbMATH — the first resource for mathematics

A concurrent lambda calculus with futures. (English) Zbl 1110.68023
Summary: We introduce a new lambda calculus with futures, $$\lambda (\text{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 (\text{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 (\text{fut})$$ is sufficiently powerful to support explicit recursion and call-by-need evaluation.
We present a static type system for $$\lambda (\text{fut})$$ and distinguish a fragment of $$\lambda (\text{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 (\text{fut})$$’s handled future-construct.
Finally, we present a linear type system for $$\lambda (\text{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.

##### MSC:
 68N18 Functional programming and lambda calculus 68Q55 Semantics in the theory of computing
##### Keywords:
functional programming languages; semantics; concurrency
##### Software:
Oz; Multilisp; Pict; JoCaml
Full Text:
##### References:
 [1] Abadi, M.; Lamport, L., Conjoining specifications, ACM trans. programming languages and systems, 17, 3, 507-534, (1995) [2] Ariola, Z.M.; Felleisen, M., The call-by-need lambda calculus, J. funct. programming, 7, 3, 265-301, (1997) · Zbl 0887.68007 [3] Ariola, Z.M.; Klop, J.W., Lambda calculus with explicit recursion, Inform. and comput., 139, 2, 154-233, (1997) · Zbl 0892.68015 [4] Arvind; Nikhil, R.S.; Pingali, K.K., I-structures: data structures for parallel computing, ACM trans. programming languages and systems, 11, 4, 598-632, (1989) [5] Baker, H.; Hewitt, C., The incremental garbage collection of processes, ACM sigplan notices, 12, 55-59, (1977) [6] E. Barendsen, S. Smetsers, Uniqueness type inference, in: Proc. PLILP’95, Lecture Notes in Computer Science, Vol. 982, Springer, 1995, pp. 189-206. · Zbl 0910.68096 [7] G. Boudol, The $$\pi$$-calculus in direct style, in: 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997, pp. 228-241. [8] Caromel, D.; Henrio, L., A theory of distributed objects, (2005), Springer Berlin · Zbl 1084.68012 [9] E. Chailloux, P. Manoury, B. Pagano, Developing Applications With Objective Caml, O’Reilly, 2000, available online at $$\langle$$http://caml.inria.fr/oreilly-book⟩. [10] S. Conchon, F.L. Fessant, Jocaml: mobile agents for objective-caml, in: First International Symposium on Agent Systems and Applications (ASA’99)/Third International Symposium on Mobile Agents (MA’99), 1999. [11] Flanagan, C.; Felleisen, M., The semantics of future and an application, J. funct. programming, 9, 1, 1-31, (1999) · Zbl 0926.68075 [12] Fournet, C.; Gonthier, G., The reflexive chemical abstract machine and the join-calculus, (), 372-385 [13] C. Fournet, C. Laneve, L. Maranget, D. Rémy, Implicit typing à la ML for the join-calculus, in: Proceedings of the CONCUR’97, Lecture Notes in Computer Science, Vol. 1243, Springer, Berlin, 1997, pp. 196-212. [14] Halstead, R.H., Multilisp: a language for concurrent symbolic computation, ACM trans. programming languages and systems, 7, 4, 501-538, (1985) · Zbl 0581.68037 [15] Haridi, S.; Van Roy, P.; Brand, P.; Mehl, M.; Scheidhauer, R.; Smolka, G., Efficient logic variables for distributed computing, ACM trans. programming languages and systems, 21, 3, 569-626, (1999) [16] Jeffrey, A.; Rathke, J., A fully abstract may testing semantics for concurrent objects, (), 101-112 [17] Jones, S.P.; Gordon, A.; Finne, S., Concurrent Haskell, (), 295-308 [18] Kobayashi, N.; Pierce, B.C.; Turner, D.N., Linearity and the pi-calculus, ACM trans. programming languages and systems, 21, 5, 914-947, (1999) [19] Landin, P.J., The mechanical evaluation of expressions, Comput. J., 6, 4, 308-320, (1964) · Zbl 0122.36106 [20] Liskov, B.; Shrira, L., Promises: linguistic support for efficient asynchronous procedure calls in distributed systems, SIGPLAN notices, 23, 7, 260-267, (1988) [21] Maraist, J.; Odersky, M.; Wadler, P., The call-by-need lambda calculus, J. funct. programming, 8, 3, 275-317, (1998) · Zbl 0918.03019 [22] R. Milner, The polyadic $$\pi$$-calculus: a tutorial, in: F.L. Bauer, W. Brauer, H. Schwichtenberg (Eds.), Logic and Algebra of Specification, Proc. Marktoberdorf Summer School, Springer, Berlin, 1993, pp. 203-246. [23] Milner, R.; Tofte, M.; Harper, R.; MacQueen, D.B., The standard ML programming language (revised), (1997), MIT Press Cambridge, MA [24] Moreau, L., The semantics of scheme with future, (), 146-156 · Zbl 1345.68066 [25] M. Müller, Set-based failure diagnosis for concurrent constraint programming, Ph.D. Thesis, Saarland University, Saarbrücken, 1998. [26] Niehren, J., Uniform confluence in concurrent computation, J. funct. programming, 10, 5, 453-499, (2000) · Zbl 0974.68061 [27] J. Niehren, J. Schwinghammer, G. Smolka, A concurrent lambda calculus with futures, in: B. Gramlich (Ed.), Frontiers of Combining Systems, Lecture Notes in Artificial Intelligence, Vol. 3717, Springer, Berlin, 2005, pp. 248-263. · Zbl 1171.68409 [28] F. Nielson (Ed.), ML with Concurrency: Design, Analysis, Implementation, and Application, Monographs in Computer Science, Springer, Berlin, 1997. [29] Pierce, B.C.; Turner, D.N., Pict: a programming language based on the pi-calculus, () [30] Reppy, J.H., Concurrent programming in ML, (1999), Cambridge University Press Cambridge · Zbl 1137.68409 [31] A. Rossberg, Generativity and dynamic opacity for abstract types, in: Proc. Fifth Internat. ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP’03), ACM Press, New York, 2003, pp. 241-252. [32] A. Rossberg, The missing link—dynamic components for ML, in: Eleventh International Conference on Fuctional Programming, ACM Press 2006. [33] A. Rossberg, D.L. Botlan, G. Tack, T. Brunklaus, G. Smolka, Alice through the looking glass, Trends in Functional Programming, Vol. 5, Intellect Books, Bristol, UK, Munich, Germany, 2006 pp. 77-96 (Chapter 6) (ISBN 1-84150144-1). [34] Saraswat, V.A.; Rinard, M.; Panangaden, P., Semantic foundations of concurrent constraint programming, (), 333-352 [35] Shapiro, E., The family of concurrent logic programming languages, ACM comput. surveys, 21, 3, 413-510, (1989) [36] G. Smolka, The Oz programming model, in: J. van Leeuwen (Ed.), Computer Science Today, Lecture Notes in Computer Science, Vol. 1000, Springer, Berlin, 1995, pp. 324-343. [37] G. Tack, L. Kornstaedt, G. Smolka, Generic pickling and minimization, ENTCS 148 (2) (2006) 79-103. [38] The Alice Project, web site at the Programming Systems Lab, Saarland University $$\langle$$http://www.ps.uni-sb.de/alice⟩, 2006. [39] Turner, D.N.; Wadler, P.; Mossin, C., Once upon a type, (), 1-11 [40] P.Wadler, Linear types can change the world!, in: M.Broy, C.B. Jones(Eds.), Programming Concepts and Methods, 1990 North-Holland, Amsterdam, pp.546-566. [41] Wright, A.K., Simple imperative polymorphism, Lisp and symbolic comput., 8, 4, 343-355, (1995)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.