{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T20:35:06Z","timestamp":1761510906997},"reference-count":53,"publisher":"Cambridge University Press (CUP)","issue":"4-5","license":[{"start":{"date-parts":[[2007,7,1]],"date-time":"2007-07-01T00:00:00Z","timestamp":1183248000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2007,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Existing languages provide good support for typeful programming of stand-alone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct programs, sharing some (but not necessarily all) of their module structure, and with some instances rebuilt with new versions of certain modules as time goes on. In this paper, we discuss programming-language support for such systems, focussing on their typing and naming issues. We describe an experimental language, Acute, which extends an ML core to support distributed development, deployment, and execution, allowing type-safe interaction between separately built programs. The main features are (1) type-safe marshalling of arbitrary values; (2) type names that are generated (freshly and by hashing) to ensure that type equality tests suffice to protect the invariants of abstract types, across the entire distributed system; (3) expression-level names generated to ensure that name equality tests suffice for type safety of associated values, for example, values carried on named channels; (4) controlled dynamic rebinding of marshalled values to local resources; and (5) thunkification of threads and mutexes to support computation mobility. These features are a large part of what is needed for typeful distributed programming. They are a relatively lightweight extension of ML, should be efficiently implementable, and are expressive enough to enable a wide variety of distributed infrastructure layers to be written as simple library code above the byte-string network and persistent store APIs. This disentangles the language run-time from communication intricacies. This paper highlights the main design choices in Acute. It is supported by a full language definition (of typing, compilation, and operational semantics), by a prototype implementation, and by example distribution libraries.<\/jats:p>","DOI":"10.1017\/s0956796807006442","type":"journal-article","created":{"date-parts":[[2007,7,9]],"date-time":"2007-07-09T13:28:51Z","timestamp":1183987731000},"page":"547-612","source":"Crossref","is-referenced-by-count":28,"title":["Acute: High-level programming language design for distributed computation"],"prefix":"10.1017","volume":"17","author":[{"given":"PETER","family":"SEWELL","sequence":"first","affiliation":[]},{"given":"JAMES J.","family":"LEIFER","sequence":"additional","affiliation":[]},{"given":"KEITH","family":"WANSBROUGH","sequence":"additional","affiliation":[]},{"given":"FRANCESCO ZAPPA","family":"NARDELLI","sequence":"additional","affiliation":[]},{"given":"MAIR","family":"ALLEN-WILLIAMS","sequence":"additional","affiliation":[]},{"given":"PIERRE","family":"HABOUZIT","sequence":"additional","affiliation":[]},{"given":"VIKTOR","family":"VAFEIADIS","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2007,7,1]]},"reference":[{"key":"S0956796807006442_ref53","unstructured":"Weirich S. (2002). Programming With Types, Ph.D. thesis. Ithaca, NY: Cornell University."},{"key":"S0956796807006442_ref52","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/360204.360214","volume-title":"Proc. 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).","author":"Unyapoth","year":"2001"},{"key":"S0956796807006442_ref51","first-page":"278","volume-title":"Proc. CONCUR LNCS 1119","author":"Thomsen","year":"1996"},{"key":"S0956796807006442_ref50","unstructured":"Stoyle G. (2006) A Theory of Dynamic Software Updates, Ph.D. thesis. Cambridge, England: University of Cambridge."},{"key":"S0956796807006442_ref46","doi-asserted-by":"crossref","unstructured":"Sewell P. , Leifer J. J. , Wansbrough K. , Allen-Williams M. , Zappa Nardelli F. , Habouzit P. & Vafeiadis V. (2005a) Source release of the Acute system. Available at: http:\/\/www.cl.cam.ac.uk\/users\/pes20\/acute\/.","DOI":"10.1145\/1090189.1086370"},{"key":"S0956796807006442_ref44","doi-asserted-by":"crossref","unstructured":"Sewell P. , Wojciechowski P. T. & Pierce B. C. (1999) Location-independent communication for mobile agents: a two-level architecture. In Internet Programming Languages, LNCS 1686. pp. 1\u201331.","DOI":"10.1007\/3-540-47959-7_1"},{"key":"S0956796807006442_ref49","first-page":"263","volume-title":"Proc. 8th ACM SIGPLAN International Conference on Functional Programming (ICFP)","author":"Shinwell","year":"2003"},{"key":"S0956796807006442_ref42","unstructured":"Sewell P. (2000) Applied \u03c0\u2014A Brief Tutorial. Tech. Rept. 498. Computer Laboratory, University of Cambridge. An extract appeared as Chapter 9, Formal Methods for Distributed Processing, A Survey of Object-oriented Approaches."},{"key":"S0956796807006442_ref40","first-page":"79","volume-title":"Trends in Functional Programming","author":"Rossberg","year":"2006"},{"key":"S0956796807006442_ref39","first-page":"241","volume-title":"Proc. 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP).","author":"Rossberg","year":"2003"},{"key":"S0956796807006442_ref35","first-page":"1","article-title":"Local type inference","volume":"22","author":"Pierce","year":"1998","journal-title":"Proc. POPL."},{"key":"S0956796807006442_ref30","volume-title":"The definition of Standard ML.","author":"Milner","year":"1990"},{"key":"S0956796807006442_ref28","doi-asserted-by":"crossref","unstructured":"Leifer J. J. , Peskine G. , Sewell P. & Wansbrough K. (2003b) Global Abstraction-Safe Marshalling With Hash Types. Tech. Rept. RR-4851. INRIA Rocquencourt. Available at: http:\/\/moscova.inria.fr\/leifer\/research.html. Also published as UCAM-CL-TR-569.","DOI":"10.1145\/944705.944714"},{"key":"S0956796807006442_ref27","first-page":"87","volume-title":"Proc. 8th ACM SIGPLAN International Conference on Functional Programming (ICFP)","author":"Leifer","year":"2003"},{"key":"S0956796807006442_ref25","doi-asserted-by":"crossref","unstructured":"Le Fessant F. (2001) Detecting distributed cycles of garbage in large-scale systems. In Proc. Principles of Distributed Computing (PODC).","DOI":"10.1145\/383962.384018"},{"key":"S0956796807006442_ref19","volume-title":"Advanced Topics in Types and Programming Languages","author":"Harper","year":"2005"},{"key":"S0956796807006442_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/371880.371887"},{"key":"S0956796807006442_ref16","unstructured":"Furuse J. & Weis P. (2000) Entr\u00e9es\/sorties de valeurs en Caml. In Proc. Journ\u00e9es francophones des langages applicatifs, pp. 79\u201398. http:\/\/jfla.inria.fr\/2000\/actes.html."},{"key":"S0956796807006442_ref15","first-page":"406","volume-title":"Proc. CONCUR, LNCS 1119.","author":"Fournet","year":"1996"},{"key":"S0956796807006442_ref14","first-page":"147","volume-title":"Proc. 14th IEEE Symp. on Logic in Computer Science (LICS).","author":"Drossopoulou","year":"1999"},{"key":"S0956796807006442_ref20","volume-title":"Proof, Language and Interaction: Essays in Honour of Robin Milner.","author":"Harper","year":"2000"},{"key":"S0956796807006442_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.02.036"},{"key":"S0956796807006442_ref7","volume-title":"ULM: A core programming model for global computing.","author":"Boudol","year":"2003"},{"key":"S0956796807006442_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/1159876.1159881"},{"key":"S0956796807006442_ref1","unstructured":"The Acute team. (2005) Acute. Available at: http:\/\/www.cl.cam.ac.uk\/users\/pes20\/acute."},{"key":"S0956796807006442_ref3","first-page":"415","volume-title":"Proc. 16th European Conference on Object-Oriented Programming (ECOOP)","author":"Benton","year":"2002"},{"key":"S0956796807006442_ref11","first-page":"22","volume-title":"Proc. 1st International Symposium on Agent Systems and Applications\/3rd International Symposium on Mobile Agents (ASA\/MA)","author":"Conchon","year":"1999"},{"key":"S0956796807006442_ref47","doi-asserted-by":"crossref","unstructured":"Sewell P. , Leifer J. J. , Wansbrough K. , Zappa Nardelli F. , Allen-Williams M. , Habouzit P. & Vafeiadis V . (2005b) Acute: High-level programming language design for distributed computation. In Proceedings of ICFP 2005: International Conference on Functional Programming (Tallinn).","DOI":"10.1145\/1086365.1086370"},{"key":"S0956796807006442_ref37","unstructured":"R\u00e9my D. (2002) Using, understanding, and unraveling the ocaml language. In Applied Semantics. Advanced Lectures. LNCS 2395, Barthe G. (ed). pp. 413\u2013537."},{"key":"S0956796807006442_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/174675.176926"},{"key":"S0956796807006442_ref21","first-page":"241","volume-title":"Proc. Foundations of Software Science and Computation Structure (FoSSaCS), part of ETAPS, LNCS 2987.","author":"Hennessy","year":"2004"},{"key":"S0956796807006442_ref38","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511574962"},{"key":"S0956796807006442_ref2","volume-title":"Concurrent Programming in Erlang","author":"Armstrong","year":"1996"},{"key":"S0956796807006442_ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35261-9_3"},{"key":"S0956796807006442_ref24","first-page":"27","volume-title":"Proceedings of the International Conference on Functional Programming (ICFP","author":"Le Botlan","year":"2003"},{"key":"S0956796807006442_ref5","volume-title":"A Bytecode Compiler for Acute","author":"Billings","year":"2005"},{"key":"S0956796807006442_ref36","volume-title":"Proof, Language and Interaction: Essays in Honour of Robin Milner.","author":"Pierce","year":"2000"},{"key":"S0956796807006442_ref13","unstructured":"Dot03. (2003). Packacking and Deploying .Net Framework Applications (.Net Framework Tutorials, MSDN), http:\/\/msdn2.microsoft.com\/cn-us\/library\/aa309395(V5.71).aspx."},{"key":"S0956796807006442_ref48","volume-title":"The Fresh Approach: Functional Programming With Names and Binders.","author":"Shinwell","year":"2005"},{"key":"S0956796807006442_ref33","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158529"},{"key":"S0956796807006442_ref10","first-page":"140","volume-title":"Proc. Foundations of Software Science and Computation Structure (FoSSaCS), LNCS 1378","author":"Cardelli","year":"1998"},{"key":"S0956796807006442_ref45","unstructured":"Sewell P. , Leifer J. J. , Wansbrough K. , Allen-Williams M. , Nardelli Z. , Francesco Habouzit P. & Vafeiadis V. (2004) Acute: High-level Programming Language Design for Distributed Computation. Design Rationale and Language Definition. Tech. Rept. 605. Cambridge, England: Computer Laboratory, University of Cambridge. Also published as INRIA RR-5329, 193pp."},{"key":"S0956796807006442_ref4","first-page":"99","volume-title":"Proc. 8th ACM SIGPLAN International Conference on Functional Programming (ICFP)","author":"Bierman","year":"2003"},{"key":"S0956796807006442_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199516"},{"key":"S0956796807006442_ref12","doi-asserted-by":"crossref","unstructured":"Deni\u00e9lou P.-M. & Leifer J. J. (2006) Abstraction preservation and subtyping in distributed languages. In Proc.@ 11th ICFP.","DOI":"10.1145\/1159803.1159841"},{"key":"S0956796807006442_ref43","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/360204.360225","volume-title":"Proc. 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).","author":"Sewell","year":"2001"},{"key":"S0956796807006442_ref32","doi-asserted-by":"publisher","DOI":"10.1145\/373243.360207"},{"key":"S0956796807006442_ref23","unstructured":"Hosoya H. , & Pierce B. C. (1999) How Good Is Local Type Inference? Tech. Rept. MS-CIS-99-17. Philadalphia: University of Pennsylvania."},{"key":"S0956796807006442_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/174675.176927"},{"key":"S0956796807006442_ref26","first-page":"173","volume-title":"Proc. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).","author":"Lee","year":"2007"},{"key":"S0956796807006442_ref31","first-page":"286","volume-title":"Proc. 19th IEEE Symp. on Logic in Computer Science (LICS).","author":"Murphy","year":"2004"},{"key":"S0956796807006442_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-30852-4"},{"key":"S0956796807006442_ref34","unstructured":"Peskine G. (Forthcoming) HOS: un calcul de modules adapt\u00e9 aux environnements r\u00e9partis. Ph.D. thesis."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796807006442","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,18]],"date-time":"2021-08-18T21:39:31Z","timestamp":1629322771000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796807006442\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,7]]},"references-count":53,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2007,7]]}},"alternative-id":["S0956796807006442"],"URL":"https:\/\/doi.org\/10.1017\/s0956796807006442","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,7]]}}}