No more, no less: A formal model for serverless computing

Maurizio Gabbrielli, Saverio Giallorenzo*, Ivan Lanese, Fabrizio Montesi, Marco Peressotti, Stefano Pio Zingaro

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

122 Downloads (Pure)


Serverless computing, also known as Functions-as-a-Service, is a recent paradigm aimed at simplifying the programming of cloud applications. The idea is that developers design applications in terms of functions, which are then deployed on a cloud infrastructure. The infrastructure takes care of executing the functions whenever requested by remote clients, dealing automatically with distribution and scaling with respect to inbound traffic. While vendors already support a variety of programming languages for serverless computing (e.g. Go, Java, Javascript, Python), as far as we know there is no reference model yet to formally reason on this paradigm. In this paper, we propose the first core formal programming model for serverless computing, which combines ideas from both the λ-calculus (for functions) and the π-calculus (for communication). To illustrate our proposal, we model a real-world serverless system. Thanks to our model, we capture limitations of current vendors and formalise possible amendments.

Original languageEnglish
Title of host publicationCoordination Models and Languages. COORDINATION 2019
EditorsH. Riis Nielson, E. Tuosto
Publication date2019
ISBN (Print)978-3-030-22396-0
ISBN (Electronic)978-3-030-22397-7
Publication statusPublished - 2019
Event21st International Conference on Coordination Models and Languages - Copenhagen, Denmark
Duration: 17. Jun 201921. Jun 2019
Conference number: 21


Conference21st International Conference on Coordination Models and Languages
SeriesLecture Notes in Computer Science


  • Serverless computing
  • Cloud computing
  • Edge computing
  • Process calculi
  • Programming languages
  • Semantics
  • Formal methods


Dive into the research topics of 'No more, no less: A formal model for serverless computing'. Together they form a unique fingerprint.

Cite this