{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,7]],"date-time":"2026-04-07T21:55:31Z","timestamp":1775598931017,"version":"3.50.1"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1413985, CCF-1453474, and CNS-1513055"],"award-info":[{"award-number":["CNS-1413985, CCF-1453474, and CNS-1513055"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>Serverless computing (also known as functions as a service) is a new cloud computing abstraction that makes it easier to write robust, large-scale web services. In serverless computing, programmers write what are called serverless functions, which are programs that respond to external events. When demand for the serverless function spikes, the platform automatically allocates additional hardware and manages load-balancing; when demand falls, the platform silently deallocates idle resources; and when the platform detects a failure, it transparently retries affected requests. In 2014, Amazon Web Services introduced the first serverless platform, AWS Lambda, and similar abstractions are now available on all major cloud computing platforms.<\/jats:p>\n          <jats:p>\n            Unfortunately, the serverless computing abstraction exposes several low-level operational details that make it hard for programmers to write and reason about their code. This paper sheds light on this problem by presenting \u03bb\n            <jats:sub>\u03bb<\/jats:sub>\n            , an operational semantics of the essence of serverless computing. Despite being a small (half a page) core calculus, \u03bb\n            <jats:sub>\u03bb<\/jats:sub>\n            models all the low-level details that serverless functions can observe. To show that \u03bb\n            <jats:sub>\u03bb<\/jats:sub>\n            is useful, we present three applications. First, to ease reasoning about code, we present a simplified naive semantics of serverless execution and precisely characterize when the naive semantics and \u03bb\n            <jats:sub>\u03bb<\/jats:sub>\n            coincide. Second, we augment \u03bb\n            <jats:sub>\u03bb<\/jats:sub>\n            with a key-value store to allow reasoning about stateful serverless functions. Third, since a handful of serverless platforms support serverless function composition, we show how to extend \u03bb\n            <jats:sub>\u03bb<\/jats:sub>\n            with a composition language and show that our implementation can outperform prior work.\n          <\/jats:p>","DOI":"10.1145\/3360575","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":75,"title":["Formal foundations of serverless computing"],"prefix":"10.1145","volume":"3","author":[{"given":"Abhinav","family":"Jangda","sequence":"first","affiliation":[{"name":"University of Massachusetts Amherst, USA"}]},{"given":"Donald","family":"Pinckney","sequence":"additional","affiliation":[{"name":"University of Massachusetts Amherst, USA"}]},{"given":"Yuriy","family":"Brun","sequence":"additional","affiliation":[{"name":"University of Massachusetts Amherst, USA"}]},{"given":"Arjun","family":"Guha","sequence":"additional","affiliation":[{"name":"University of Massachusetts Amherst, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"SAND: Towards High-Performance Serverless Computing. In USENIX Annual Technical Conference (ATC).","author":"Akkus Istemi Ekin","year":"2018"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276488"},{"key":"e_1_2_2_3_1","volume-title":"AWS Lambda Developer Guide: Invoke. https:\/\/docs.aws.amazon.com\/lambda\/latest\/dg\/API_Invoke.html . Accessed","author":"Amazon","year":"2018"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3267809.3267815"},{"key":"e_1_2_2_5_1","volume-title":"Supporting Multi-Provider Serverless Computing on the Edge. In International Conference on Parallel Processing (ICPP) .","author":"Aske Austin","year":"2018"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133934"},{"key":"e_1_2_2_7_1","volume-title":"The Serverless Trilemma: Function Composition for Serverless Computing. In ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward!) .","author":"Baldini Ioana","year":"2017"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276954.3276958"},{"key":"e_1_2_2_9_1","unstructured":"Phil Bernstein Sergey Bykov Alan Geller and Jorgen Thelin. 2014. Orleans: Distributed Virtual Actors for Programmability and Scalability . Technical Report. https:\/\/www.microsoft.com\/en-us\/research\/publication\/orleans-distributed-virtualactors-for-programmability-and-scalability\/  Phil Bernstein Sergey Bykov Alan Geller and Jorgen Thelin. 2014. Orleans: Distributed Virtual Actors for Programmability and Scalability . Technical Report. https:\/\/www.microsoft.com\/en-us\/research\/publication\/orleans-distributed-virtualactors-for-programmability-and-scalability\/"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/NOMS.2016.7502933"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2889443.2889452"},{"key":"e_1_2_2_12_1","volume-title":"USENIX Symposium on Operating Systems Design and Implementation (OSDI).","author":"Chajed Tej","year":"2018"},{"key":"e_1_2_2_13_1","volume-title":"Cloud Native Technologies Are Scaling Production Applications. https:\/\/www.cncf.io\/blog\/2017\/12\/ 06\/cloud-native-technologies-scaling-production-applications\/ . Accessed","author":"Conway Sarah","year":"2018"},{"key":"e_1_2_2_14_1","volume-title":"Compositional Programming and Testing of Dynamic Distributed Systems. In ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages and Applications (OOPSLA) .","author":"Desai Ankush"},{"key":"e_1_2_2_15_1","volume-title":"PSync: A Partially Synchronous Language for Faulttolerant Distributed Algorithms. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL).","author":"Dr\u0103goi Cezara","year":"2016"},{"key":"e_1_2_2_16_1","volume-title":"https:\/\/www.openfaas.com . Accessed","author":"Ellis Alex","year":"2018"},{"key":"e_1_2_2_17_1","volume-title":"Proceedings of the IFIP TC 2\/WG 2.2 Working Conference on Formal Description of Programming Concepts .","author":"Felleisen Matthias"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254096"},{"key":"e_1_2_2_19_1","unstructured":"Sadjad Fouladi Francisco Romero Dan Iter Qian Li Shuvo Chatterjee Christos Kozyrakis Matei Zaharia and Keith Winstein. 2019. From Laptop to Lambda: Outsourcing Everyday Jobs to Thousands of Transient Functional Containers.  Sadjad Fouladi Francisco Romero Dan Iter Qian Li Shuvo Chatterjee Christos Kozyrakis Matei Zaharia and Keith Winstein. 2019. From Laptop to Lambda: Outsourcing Everyday Jobs to Thousands of Transient Functional Containers."},{"key":"e_1_2_2_20_1","volume-title":"Fast and Slow: Low-Latency Video Processing Using Thousands of Tiny Threads. In USENIX Symposium on Networked System Design and Implementation (NSDI).","author":"Fouladi Sadjad","year":"2017"},{"key":"e_1_2_2_21_1","volume-title":"Proceedings of the ACM on Programming Languages 2, POPL","author":"Santos Jos\u00e9 Fragoso","year":"2018"},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","unstructured":"Maurizio Gabbrielli Saverio Giallorenzo Ivan Lanese Fabrizio Montesi Marco Peressotti and Stefano Pio Zingaro. 2019. No More No Less - A Formal Model for Serverless Computing. In Coordination Models and Languages (COORDINATION). 148\u2013157.  Maurizio Gabbrielli Saverio Giallorenzo Ivan Lanese Fabrizio Montesi Marco Peressotti and Stefano Pio Zingaro. 2019. No More No Less - A Formal Model for Serverless Computing. In Coordination Models and Languages (COORDINATION). 148\u2013157.","DOI":"10.1007\/978-3-030-22397-7_9"},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","unstructured":"Yu Gan and Christina Delimitrou. 2018. The Architectural Implications of Cloud Microservices. In Computer Architecture Letters (CAL) .  Yu Gan and Christina Delimitrou. 2018. The Architectural Implications of Cloud Microservices. In Computer Architecture Letters (CAL) .","DOI":"10.1109\/LCA.2018.2839189"},{"key":"e_1_2_2_24_1","volume-title":"Verifying Strong Eventual Consistency in Distributed Systems. In ACM SIGPLAN Conference on Object Oriented Programming, Systems, Languages and Applications (OOPSLA) .","author":"Gomes Victor B. F."},{"key":"e_1_2_2_25_1","volume-title":"Cloud Functions Execution Environment. https:\/\/cloud.google.com\/functions\/docs\/concepts\/exec . Accessed","author":"Google","year":"2018"},{"key":"e_1_2_2_26_1","volume-title":"Google Cloud Functions. https:\/\/cloud.google.com\/functions\/ . Accessed","author":"Google","year":"2018"},{"key":"e_1_2_2_27_1","volume-title":"Machine Verified Network Controllers. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) .","author":"Guha Arjun","year":"2013"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_2_29_1","volume-title":"USENIX Workshop on Hot Topics in Cloud Computing (HotCloud) .","author":"Hendrickson Scott"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00023-4"},{"key":"e_1_2_2_31_1","unstructured":"Abhinav Jangda Donald Pinckney Yuriy Brun and Arjun Guha. 2019. Formal Foundations of Serverless Computing. https:\/\/arxiv.org\/abs\/1902.05870 .  Abhinav Jangda Donald Pinckney Yuriy Brun and Arjun Guha. 2019. Formal Foundations of Serverless Computing. https:\/\/arxiv.org\/abs\/1902.05870 ."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127479.3128601"},{"key":"e_1_2_2_33_1","volume-title":"Choose between Azure services that deliver messages. https:\/\/docs.microsoft.com\/en-us\/azure\/eventgrid\/compare-messaging-services . Accessed","author":"Microsoft","year":"2018"},{"key":"e_1_2_2_34_1","volume-title":"Microsoft Azure Functions. https:\/\/azure.microsoft.com\/en-us\/services\/functions\/ . Accessed","author":"Microsoft","year":"2018"},{"key":"e_1_2_2_35_1","volume-title":"https:\/\/openwhisk.apache.org . Accessed","author":"Apache OpenWhisk OpenWhisk","year":"2018"},{"key":"e_1_2_2_36_1","volume-title":"https:\/\/github.com\/apache\/incubator-openwhisk\/blob\/master\/docs\/actions.md . Accessed","author":"OpenWhisk Actions OpenWhisk","year":"2018"},{"key":"e_1_2_2_37_1","volume-title":"Verification in the Age of Microservices. In Workshop on Hot Topics in Operating Systems .","author":"Panda Aurojit","year":"2017"},{"key":"e_1_2_2_38_1","volume-title":"KJS: A Complete Formal Semantics of JavaScript. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) .","author":"Park Daejun","year":"2015"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507664"},{"key":"e_1_2_2_40_1","volume-title":"Cloud Native Infrastructure as Code. https:\/\/www.pulumi.com\/ . Accessed","author":"Pulumi Pulumi","year":"2018"},{"key":"e_1_2_2_41_1","volume-title":"Composing Functions into Applications the Serverless Way. https:\/\/medium.com\/openwhisk\/ composing-functions-into-applications-70d3200d0fac . Accessed","author":"Rabbah Rodric","year":"2018"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429100"},{"key":"e_1_2_2_43_1","volume-title":"Programming and Proving with Distributed Protocols. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) .","author":"Sergey Ilya","year":"2017"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304016"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3152434.3152450"},{"key":"e_1_2_2_46_1","volume-title":"Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming.","author":"Walker David"},{"key":"e_1_2_2_47_1","volume-title":"Whip: Higher-Order Contracts for Modern Services. In ACM International Conference on Functional Programming (ICFP) .","author":"Waye Lucas","year":"2017"},{"key":"e_1_2_2_48_1","doi-asserted-by":"crossref","unstructured":"Sanjiva Weerawarana Chathura Ekanayake Srinath Perera and Frank Leymann. 2018. Bringing Middleware to Everyday Programmers with Ballerina. In Business Process Management.  Sanjiva Weerawarana Chathura Ekanayake Srinath Perera and Frank Leymann. 2018. Bringing Middleware to Everyday Programmers with Ballerina. In Business Process Management.","DOI":"10.1007\/978-3-319-98648-7_2"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360575","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360575","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360575","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360575"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":49,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360575"],"URL":"https:\/\/doi.org\/10.1145\/3360575","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}