A picture of Marco

About

I am Marco Peressotti and I am an Associate Professor of Computer Science at the Department of Mathematics and Computer Science of the University of Southern Denmark where I am member of the Section of Artificial Intelligence, Cybersecurity, and Programming Languages. I also serve as member of the Communication Group of the Microservices Community, an international community of researchers, professionals, and students interested in the software paradigm of Microservices. I received my Ph.D. Degree in Computer Science from the University of Udine in 2017.

My research mission is to make it more effective and robust to program and analyse concurrent systems. An overarching theme of my research approach is the use of formal methods and programming languages techniques as well as the aim for a unifying mathematical perspective rooted in Logic and Category Theory.

Highlights

Jun'24
I gave a lecture about Microservices and Distributed Transactions at BankData.
Mar'24
I gave an introduction to Software Verification with TLA+ for the participants of the Danish Cyber Championships.
Mar'24
I gave an introduction to Formal Methods and a tutorial on TLA+ at SecureTech, a workshop for professionals organised by the Danish Centre for Cyber Security and DigitalLead.
Jan'24
I gave a talk about on “Probabilistic Theories of Choreographic Programming” at the Dagstuhl Seminar Next Generation Protocols for Heterogeneous Systems.
Dec'23
I will co-chair the 1st International Workshop on Choreographic Programming (CP 2024), co-located with PLDI 2024.
Oct'23
Our paper “Choral: Object-Oriented Choreographic Programming” was accepted for publication in ACM Transactions on Programming Languages and Systems (TOPLAS).

All news

Selected publications

Giallorenzo, S., Montesi, F. and Peressotti, M. 2024. Choral: Object-oriented Choreographic Programming. ACM Trans. Program. Lang. Syst. 46, 1 (2024), 1:1–1:59. DOI:10.1145/3632398.

Choreographies are coordination plans for concurrent and distributed systems, which define the roles of the involved participants and how they are supposed to work together. In the paradigm of choreographic programming, choreographies are programs that can be compiled into executable implementations.

In this article, we present Choral, the first choreographic programming language based on mainstream abstractions. The key idea in Choral is a new notion of data type, which allows for expressing that data is distributed over different roles. We use this idea to reconstruct the paradigm of choreographic programming through object-oriented abstractions. Choreographies are classes, and instances of choreographies are objects with states and behaviours implemented collaboratively by roles.

Choral comes with a compiler that, given a choreography, generates an implementation for each of its roles. These implementations are libraries in pure Java, whose types are under the control of the Choral programmer. Developers can then modularly compose these libraries in their programs, to participate correctly in choreographies. Choral is the first incarnation of choreographic programming offering such modularity, which finally connects more than a decade of research on the paradigm to practical software development.

The integration of choreographic and object-oriented programming yields other powerful advantages, where the features of one paradigm benefit the other in ways that go beyond the sum of the parts. On the one hand, the high-level abstractions and static checks from the world of choreographies can be used to write concurrent and distributed object-oriented software more concisely and correctly. On the other hand, we obtain a much more expressive choreographic language from object-oriented abstractions than in previous work. This expressivity allows for writing more reusable and flexible choreographies. For example, object passing makes Choral the first higher-order choreographic programming language, whereby choreographies can be parameterised over other choreographies without any need for central coordination. We also extend method overloading to a new dimension: specialisation based on data location. Together with subtyping and generics, this allows Choral to elegantly support user-defined communication mechanisms and middleware.

@article{GMP24,
  author = {Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco},
  title = {Choral: Object-oriented Choreographic Programming},
  year = {2024},
  issue_date = {March 2024},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  journal = {ACM Trans. Program. Lang. Syst.},
  volume = {46},
  number = {1},
  pages = {1:1--1:59},
  issn = {0164-0925},
  url = {https://doi.org/10.1145/3632398},
  doi = {10.1145/3632398},
  keywords = {Communication, Higher-Kinded Types, Choreographies}
}
Cruz-Filipe Luı́s, Montesi, F. and Peressotti, M. 2023. A Formal Theory of Choreographic Programming. Journal of Automated Reasoning. 67, 21 (2023), 1–34. DOI:10.1007/s10817-023-09665-3.

Choreographic programming is a paradigm for writing coordination plans for distributed systems from a global point of view, from which correct-by-construction decentralised implementations can be generated automatically.

Theory of choreographies typically includes a number of complex results that are proved by structural induction. The high number of cases and the subtle details in some of these proofs has led to important errors being found in published works.

In this work, we formalise the theory of a choreographic programming language in Coq. Our development includes the basic properties of this language, a proof of its Turing completeness, a compilation procedure to a process language, and an operational characterisation of the correctness of this procedure.

Our formalisation experience illustrates the benefits of using a theorem prover: we get both an additional degree of confidence from the mechanised proof, and a significant simplification of the underlying theory. Our results offer a foundation for the future formal development of choreographic languages.

@article{CMP23,
  author = {Cruz{-}Filipe, Lu{\'{\i}}s and Montesi, Fabrizio and Peressotti, Marco},
  title = {A Formal Theory of Choreographic Programming},
  journal = {Journal of Automated Reasoning},
  volume = {67},
  number = {21},
  pages = {1--34},
  year = {2023},
  issn = {1573-0670},
  url = {https://doi.org/10.1007/s10817-023-09665-3},
  doi = {10.1007/s10817-023-09665-3}
}
Chiapperini, A., Miculan, M. and Peressotti, M. 2022. Computing (Optimal) Embeddings of Directed Bigraphs. Science of Computer Programming. 221, (2022), 102842. DOI:10.1016/j.scico.2022.102842.

Bigraphs and bigraphical reactive systems are a well-known meta-model successfully used for formalizing a wide range of models and situations, such as process calculi, service oriented architectures, multi-agent systems, biological systems, etc.. A key problem in both the theory and the implementations of bigraphs is how to compute embeddings, i.e., structure-preserving mappings of a given bigraph (the pattern or guest) inside another (the target or host). In this paper, we present an algorithm for computing embeddings for directed bigraphs, an extension of Milner’s bigraphs which take into account the request directions between controls and names. This algorithm solves the embedding problem by means of a reduction to a constraint satisfaction problem. We first prove soundness and completeness of this algorithm; then we present an implementation in jLibBig, a general Java library for manipulating bigraphical reactive systems. The effectiveness of this implementation is shown by several experimental results. Finally, we show that this algorithm can be readily adapted to find the optimal embeddings in a weighted variant of the embedding problem.

@article{CMP22,
  title = {Computing (Optimal) Embeddings of Directed Bigraphs},
  author = {Chiapperini, Alessio and Miculan, Marino and Peressotti, Marco},
  journal = {Science of Computer Programming},
  volume = {221},
  pages = {102842},
  year = {2022},
  issn = {0167-6423},
  doi = {10.1016/j.scico.2022.102842},
  url = {https://www.sciencedirect.com/science/article/pii/S0167642322000752}
}
Giallorenzo, S., Montesi, F., Peressotti, M., Richter, D., Salvaneschi, G. and Weisenburger, P. 2021. Multiparty Languages: The Choreographic and Multitier Cases. 35th European Conference on Object-Oriented Programming (ECOOP 2021) (Dagstuhl, Germany, 2021), 22:1–22:27.

Choreographic languages aim to express multiparty communication protocols, by providing primitives that make interaction manifest. Multitier languages enable programming computation that spans across several tiers of a distributed system, by supporting primitives that allow computation to change the location of execution. Rooted into different theoretical underpinnings—respectively process calculi and lambda calculus—the two paradigms have been investigated independently by different research communities with little or no contact. As a result, the link between the two paradigms has remained hidden for long.

In this paper, we show that choreographic languages and multitier languages are surprisingly similar. We substantiate our claim by isolating the core abstractions that differentiate the two approaches and by providing algorithms that translate one into the other in a straightforward way. We believe that this work paves the way for joint research and cross-fertilisation among the two communities.

@inproceedings{GMPRSW21,
  author = {Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Richter, David and Salvaneschi, Guido and Weisenburger, Pascal},
  title = {{Multiparty Languages: The Choreographic and Multitier Cases}},
  booktitle = {35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages = {22:1--22:27},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  isbn = {978-3-95977-190-0},
  issn = {1868-8969},
  year = {2021},
  volume = {194},
  editor = {M{\o}ller, Anders and Sridharan, Manu},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address = {Dagstuhl, Germany},
  url = {https://drops.dagstuhl.de/opus/volltexte/2021/14065},
  urn = {urn:nbn:de:0030-drops-140658},
  doi = {10.4230/LIPIcs.ECOOP.2021.22}
}
Cruz-Filipe Luı́s, Montesi, F. and Peressotti, M. 2021. Formalising a Turing-Complete Choreographic Language in Coq. 12th International Conference on Interactive Theorem Proving (ITP 2021) (Dagstuhl, Germany, 2021), 15:1–15:18.

Theory of choreographic languages typically includes a number of complex results that are proved by structural induction. The high number of cases and the subtle details in some of them lead to long reviewing processes, and occasionally to errors being found in published proofs. In this work, we take a published proof of Turing completeness of a choreographic language and formalise it in Coq. Our development includes formalising the choreographic language and its basic properties, Kleene’s theory of partial recursive functions, the encoding of these functions as choreographies, and proving this encoding correct. With this effort, we show that theorem proving can be a very useful tool in the field of choreographic languages: besides the added degree of confidence that we get from a mechanised proof, the formalisation process led us to a significant simplification of the underlying theory. Our results offer a foundation for the future formal development of choreographic languages.

@inproceedings{CMP21a,
  author = {Cruz-Filipe, Lu{\'\i}s and Montesi, Fabrizio and Peressotti, Marco},
  title = {{Formalising a Turing-Complete Choreographic Language in Coq}},
  booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages = {15:1--15:18},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  isbn = {978-3-95977-188-7},
  issn = {1868-8969},
  year = {2021},
  volume = {193},
  editor = {Cohen, Liron and Kaliszyk, Cezary},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address = {Dagstuhl, Germany},
  url = {https://drops.dagstuhl.de/opus/volltexte/2021/13910},
  urn = {urn:nbn:de:0030-drops-139109},
  doi = {10.4230/LIPIcs.ITP.2021.15}
}
Kokke, W., Montesi, F. and Peressotti, M. 2019. Better late than never: a fully-abstract semantics for classical processes. PACMPL. 3, POPL (2019), 24:1–24:29. DOI:10.1145/3290337.

We present Hypersequent Classical Processes (HCP), a revised interpretation of the “Proofs as Processes” correspondence between linear logic and the π-calculus initially proposed by Abramsky [1994], and later developed by Bellin and Scott [1994], Caires and Pfenning [2010], and Wadler [2014], among others. HCP mends the discrepancies between linear logic and the syntax and observable semantics of parallel composition in the π-calculus, by conservatively extending linear logic to hyperenvironments (collections of environments, inspired by the hypersequents by Avron [1991]). Separation of environments in hyperenvironments is internalised by ⊗ and corresponds to parallel process behaviour. Thanks to this property, for the first time we are able to extract a labelled transition system (lts) semantics from proof rewritings. Leveraging the information on parallelism at the level of types, we obtain a logical reconstruction of the delayed actions that Merro and Sangiorgi [2004] formulated to model non-blocking I/O in the π-calculus. We define a denotational semantics for processes based on Brzozowski derivatives, and uncover that non-interference in HCP corresponds to Fubini’s theorem of double antiderivation. Having an lts allows us to validate HCP using the standard toolbox of behavioural theory. We instantiate bisimilarity and barbed congruence for HCP, and obtain a full abstraction result: bisimilarity, denotational equivalence, and barbed congruence coincide.

@article{KMP19,
  author = {Kokke, Wen and Montesi, Fabrizio and Peressotti, Marco},
  title = {Better late than never: a fully-abstract semantics for classical processes},
  journal = {{PACMPL}},
  volume = {3},
  number = {{POPL}},
  pages = {24:1--24:29},
  year = {2019},
  url = {https://doi.org/10.1145/3290337},
  doi = {10.1145/3290337}
}

All publications