Abstract
We introduce a new concurrent lambda calculus with futures, λ (fut), to model the operational semantics of Alice, a concurrent extension of ML. λ (fut) is a minimalist extension of the call-by-value λ-calculus that yields the full expressiveness to define, combine, and implement a variety of standard concurrency constructs such as channels, semaphores, and ports. We present a linear type system for λ (fut) by which the safety of such definitions and their combinations can be proved: Well-typed implementations cannot be corrupted in any well-typed context.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abadi, M., Lamport, L.: Conjoining specifications. ACM Transactions on Programming Languages and Systems 17(3), 507–534 (1995)
The Alice Project. Web site at the Programming Systems Lab, Universität des Saarlandes (2005), http://www.ps.uni-sb.de/alice
Ariola, Z.M., Felleisen, M.: The call-by-need lambda calculus. Journal of Functional Programming 7(3), 265–301 (1997)
Arvind, R.S.N., Pingali, K.K.: I-structures: Data structures for parallel computing. ACM Transactions on Programming Languages and Systems 11(4), 598–632 (1989)
Baker, H., Hewitt, C.: The incremental garbage collection of processes. ACM Sigplan Notices 12, 55–59 (1977)
Barendsen, E., Smetsers, S.: Uniqueness type inference. In: Swierstra, S.D. (ed.) PLILP 1995. LNCS, vol. 982, pp. 189–206. Springer, Heidelberg (1995)
Chailloux, E., Manoury, P., Pagano, B.: Developing Applications With Objective Caml. O’Reilly, Sebastopol (2000), Available online at http://caml.inria.fr/oreilly-book
Conchon, S., Fessant, F.L.: Jocaml: Mobile agents for Objective-Caml. In: First International Symposium on Agent Systems and Applications (ASA 1999)/Third International Symposium on Mobile Agents (MA 1999) (1999)
Flanagan, C., Felleisen, M.: The semantics of future and an application. Journal of Functional Programming 9(1), 1–31 (1999)
Fournet, C., Gonthier, G.: The reflexive chemical abstract machine and the join-calculus. In: Proc. POPL 1996, pp. 372–385. ACM Press, New York (1996)
Fournet, C., Laneve, C., Maranget, L., Rémy, D.: Implicit typing à la ML for the join-calculus. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 196–212. Springer, Heidelberg (1997)
Halstead Jr., R.H.: Multilisp: A Language for Concurrent Symbolic Computation. ACM Transactions on Programming Languages and Systems 7(4), 501–538 (1985)
Haridi, S., Roy, P.V., Brand, P., Mehl, M., Scheidhauer, R., Smolka, G.: Efficient logic variables for distributed computing. ACM Transactions on Programming Languages and Systems 21(3), 569–626 (1999)
Liskov, B., Shrira, L.: Promises: Linguistic support for efficient asynchronous procedure calls in distributed systems. SIGPLAN Notices 23(7), 260–268 (1988)
Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus. Journal of Functional Programming 8(3), 275–317 (1998)
Milner, R.: The polyadic π-calculus: A tutorial. In: Bauer, F.L., Brauer, W., Schwichtenberg, H. (eds.) Logic and Algebra of Specification, Proc. Marktoberdorf Summer School, pp. 203–246. Springer, Heidelberg (1993)
Milner, R., Tofte, M., Harper, R., MacQueen, D.B.: The Standard ML Programming Language (Revised). MIT Press, Cambridge (1997)
Müller, M.: Set-based Failure Diagnosis for Concurrent Constraint Programming. PhD thesis, Universität des Saarlandes, Saarbrücken (1998)
Niehren, J.: Uniform confluence in concurrent computation. Journal of Functional Programming 10(5), 453–499 (2000)
Nielson, F.: ML with Concurrency: Design, Analysis, Implementation, and Application. Monographs in Computer Science. Springer, Heidelberg (1997)
Pierce, B.C., Turner, D.N.: Pict: A programming language based on the pi-calculus. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, Cambridge (2000)
Reppy, J.H.: Concurrent Programming in ML. Cambridge University Press, Cambridge (1999)
Rossberg, A., Botlan, D.L., Tack, G., Brunklaus, T., Smolka, G.: Alice Through the Looking Glass. Trends in Functional Programming, vol. 5. Intellect, Munich (2004)
Saraswat, V.A., Rinard, M., Panangaden, P.: Semantic foundations of concurrent constraint programming. In: Proc. POPL 1991, pp. 333–352. ACM Press, New York
Shapiro, E.: The family of concurrent logic programming languages. ACM Comput. Surv. 21(3), 413–510 (1989)
Smolka, G.: The Oz programming model. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol. 1000, pp. 324–343. Springer, Heidelberg (1995)
Turner, D.N., Wadler, P., Mossin, C.: Once upon a type. In: Proc. 7th ICFPCA, pp. 1–11. ACM Press, New York (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Niehren, J., Schwinghammer, J., Smolka, G. (2005). A Concurrent Lambda Calculus with Futures. In: Gramlich, B. (eds) Frontiers of Combining Systems. FroCoS 2005. Lecture Notes in Computer Science(), vol 3717. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11559306_14
Download citation
DOI: https://doi.org/10.1007/11559306_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29051-3
Online ISBN: 978-3-540-31730-2
eBook Packages: Computer ScienceComputer Science (R0)