My publications are also listed on my DBLP, Google Scholar, and Scopus profiles.

J10

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.

I12

Acclavio, M., Montesi, F. and Peressotti, M. 2024. On Propositional Dynamic Logic and Concurrency. *CoRR*. abs/2403.18508, (2024). DOI:10.48550/arXiv.2403.18508.

I11

Plyukhin, D., Montesi, F. and Peressotti, M. 2024. Ozone: Fully Out-of-Order Choreographies. *CoRR*. abs/2401.17403, (2024). DOI:10.48550/arXiv.2401.17403.

Choreographic programming is a paradigm for writing distributed applications. It allows programmers to write a single program, called a choreography, that can be compiled to generate correct implementations of each process in the application. Although choreographies provide good static guarantees, they can exhibit high latency when messages or processes are delayed. This is because processes in a choreography typically execute in a fixed, deterministic order, and cannot adapt to the order that messages arrive at runtime. In non-choreographic code, programmers can address this problem by allowing processes to execute out of order – for instance by using futures or reactive programming. However, in choreographic code, out-of-order process execution can lead to serious and subtle bugs, called communication integrity violations (CIVs).

In this paper, we develop a model of choreographic programming for out-of-order processes that guarantees absence of CIVs and deadlocks. As an application of our approach, we also introduce an API for safe non-blocking communication via futures in the choreographic programming language Choral. The API allows processes to execute out of order, participate in multiple choreographies concurrently, and to handle unordered or dropped messages as in the UDP transport protocol. We provide an illustrative evaluation of our API, showing that out-of-order execution can reduce latency by overlapping communication with computation.

J9

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.

J8

Giallorenzo, S., Montesi, F., Peressotti, M. and Rademacher, F. 2023. LEMMA2Jolie: A Tool to Generate Microservice APIs from Domain Models. *Science of Computer Programming*. 228, (2023), 102956. DOI:10.1016/j.scico.2023.102956.

C23

Giallorenzo, S., Montesi, F., Peressotti, M. and Rademacher, F. 2023. Model-Driven Code Generation for Microservices: Service Models. *Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022)* (Dagstuhl, Germany, 2023), 6:1–6:17.

C22

Cruz-Filipe Luı́s, Madsen, A., Montesi, F. and Peressotti, M. 2023. Modular Choreographies: Bridging Alice and Bob Notation to Java. *Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022)* (Dagstuhl, Germany, 2023), 3:1–3:18.

C21

Cruz-Filipe Luı́s, Graversen, E., Lugović, L., Montesi, F. and Peressotti, M. 2023. Modular Compilation for Higher-Order Functional Choreographies. *37th European Conference on Object-Oriented Programming (ECOOP 2023)* (Dagstuhl, Germany, 2023), 7:1–7:37.

C20

Giallorenzo, S., Montesi, F., Peressotti, M., Rademacher, F. and Unwerawattana, N. 2023. JoT: A Jolie Framework for Testing Microservices. *Coordination Models and Languages* (2023), 172–191.

C19

Cruz-Filipe Luı́s, Graversen, E., Montesi, F. and Peressotti, M. 2023. Reasoning About Choreographic Programs. *Coordination Models and Languages* (2023), 144–162.

Choreographic programming is a paradigm where a concurrent or distributed system is developed in a top-down fashion. Programs, called choreographies, detail the desired interactions between processes, and can be compiled to distributed implementations based on message passing. Choreographic languages usually guarantee deadlock-freedom and provide an operational correspondence between choreographies and their compiled implementations, but until now little work has been done on verifying other properties.

This paper presents a Hoare-style logic for reasoning about the behaviour of choreographies, and illustrate its usage in representative examples. We show that this logic is sound and complete, and discuss decidability of its judgements. Using existing results from choreographic programming, we show that any functional correctness property proven for a choreography also holds for its compiled implementation.

J7

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.

C18

Cruz-Filipe Luı́s, Graversen, E., Lugović, L., Montesi, F. and Peressotti, M. 2022. Functional Choreographic Programming. *Theoretical Aspects of Computing - ICTAC 2022 - 19th International Colloquium, Tbilisi, Georgia, September 27-29, 2022, Proceedings* (2022), 212–237.

C17

Giallorenzo, S., Montesi, F., Peressotti, M. and Rademacher, F. 2022. Model-Driven Generation of Microservice Interfaces: From LEMMA Domain Models to Jolie APIs. *Coordination Models and Languages* (2022), 223–240.

C16

Montesi, F., Peressotti, M. and Picotti, V. 2021. Sliceable Monolith: Monolith First, Microservices Later. *IEEE International Conference on Services Computing, SCC 2021, Chicago, IL, USA, September 5-10, 2021* (2021), 364–366.

C15

Cruz-Filipe Luı́s, Montesi, F. and Peressotti, M. 2021. Certifying Choreography Compilation. *Theoretical Aspects of Computing - ICTAC 2021 - 18th International Colloquium, Virtual Event, Nur-Sultan, Kazakhstan, September 8-10, 2021, Proceedings* (2021), 115–133.

C14

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.

C13

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.

C12

Giallorenzo, S., Montesi, F., Peressotti, M., Rademacher, F. and Sachweh, S. 2021. Jolie and LEMMA: Model-Driven Engineering and Programming Languages Meet on Microservices. *Coordination Models and Languages - 23rd IFIP WG 6.1 International Conference, COORDINATION 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings* (2021), 276–284.

I10

Cruz-Filipe Luı́s, Graversen, E., Lugović, L., Montesi, F. and Peressotti, M. 2021. Functional Choreographic Programming. *CoRR*. abs/2111.03701, (2021). DOI:10.48550/arXiv.2111.03701.

Choreographic programming is an emerging programming paradigm for concurrent and distributed systems, whereby developers write the communications that should be enacted and then a distributed implementation is automatically obtained by means of a compiler. Theories of choreographic programming typically come with strong theoretical guarantees about the compilation process, most notably: the generated implementations operationally correspond to their source choreographies and are deadlock-free.

Currently, the most advanced incarnation of the paradigm is Choral, an object-oriented choreographic programming language that targets Java. Choral deviated significantly from known theories of choreographies, and introduced the possibility of expressing higher-order choreographies (choreographies parameterised over choreographies) that are fully distributed. As a consequence, it is unclear if the usual guarantees of choreographies can still hold in the more general setting of higher-order ones.

We introduce Chorλ, the first functional choreographic programming language: it introduces a new formulation of the standard communication primitive found in choreographies as a function, and it is based upon the λ-calculus. Chorλ is the first theory that explains the core ideas of higher-order choreographic programming (as in Choral). Bridging the gap between practice and theory requires developing a new evaluation strategy and typing discipline for λ terms that accounts for the distributed nature of computation in choreographies. We illustrate the expressivity of Chorλ with a series of examples, which include reconstructions of the key examples from the original presentation of Choral. Our theory supports the expected properties of choreographic programming and bridges the gap between the communities of functional and choreographic programming.

I9

Montesi, F. and Peressotti, M. 2021. Linear Logic, the π-calculus, and their Metatheory: A Recipe for Proofs as Processes. *CoRR*. abs/2106.11818, (2021). DOI:10.48550/arXiv.2106.11818.

C11

Miculan, M. and Peressotti, M. 2020. Software Transactional Memory with Interactions. *Proceedings of the 21st Italian Conference on Theoretical Computer Science, Ischia, Italy, September 14-16, 2020* (2020), 67–80.

C10

Chiapperini, A., Miculan, M. and Peressotti, M. 2020. Computing Embeddings of Directed Bigraphs. *Graph Transformation - 13th International Conference, ICGT 2020, Held as Part of STAF 2020, Bergen, Norway, June 25-26, 2020, Proceedings* (2020), 38–56.

C9

Burco, F., Miculan, M. and Peressotti, M. 2020. Towards a Formal Model for Composable Container Systems. *Proceedings of the 35rd Annual ACM Symposium on Applied Computing, SAC 2020, Brno, Czech Republic, March 29-April 03, 2020* (2020), 173–175.

*local directed bigraphs*, a graph-based formalism which allows us to deal with localized resources. Then, we define a signature for modelling containers and provide some examples of bigraphs modelling containers. These graphs can be analysed and manipulated using techniques from graph theory: properties about containers can be formalized as properties of the corresponding bigraphic representations. Moreover, it turns out that the composition of containers as performed by e.g. docker-compose, corresponds precisely to the composition of the corresponding bigraphs inside an “environment bigraph” which in turn is obtained directly from the YAML file used to define the composition of containers.

W5

Andersen, J.L., Hellmuth, M., Merkle, D., Nøjgaard, N. and Peressotti, M. 2020. A Graph-Based Tool to Embed the π-Calculus into a Computational DPO Framework. *Proceedings of the SOFSEM 2020 Student Research Forum co-located with the 46th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM 2020)* (2020), 121–132.

E1

Cruz-Filipe Luı́s, Giallorenzo, S., Montesi, F., Peressotti, M., Rademacher, F. and Sachweh, S. eds. 2020. *Joint Post-proceedings of the First and Second International Conference on Microservices, Microservices 2017/2019, October 23-27, 2017, Odense, Denmark / February 19-21, 2019, Dortmund, Germany*. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.

I8

Giallorenzo, S., Montesi, F. and Peressotti, M. 2020. Choral: Object-Oriented Choreographic Programming. *CoRR*. abs/22005.09520, (2020). DOI:10.48550/arXiv.2005.09520.

J6

Brengos, T. and Peressotti, M. 2019. Behavioural equivalences for timed systems. *Logical Methods in Computer Science*. 15, 1 (2019). DOI:10.23638/LMCS-15(1:17)2019.

J5

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.

C8

Gabbrielli, M., Giallorenzo, S., Lanese, I., Montesi, F., Peressotti, M. and Zingaro, S.P. 2019. No More, No Less - A Formal Model for Serverless Computing. *Coordination Models and Languages - 21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17-21, 2019, Proceedings* (2019), 148–157.

I7

Brengos, T. and Peressotti, M. 2019. Two modes of recognition: algebra, coalgebra, and languages. *CoRR*. abs/1906.05573, (2019). DOI:10.48550/arXiv.1906.05573.

C7

Cruz-Filipe Luı́s, Montesi, F. and Peressotti, M. 2018. Communications in choreographies, revisited. *Proceedings of the 33rd Annual ACM Symposium on Applied Computing, SAC 2018, Pau, France, April 09-13, 2018* (2018), 1248–1255.

*monadic* setting: interaction terms express point-to-point communications of a single value. However, real-world systems often rely on interactions of *polyadic* nature, where multiple values are communicated among two or more parties, like multicast, scatter-gather, and atomic exchanges.

We introduce a new model for choreographic programming equipped with a primitive for grouped interactions that subsumes all the above scenarios. Intuitively, grouped interactions can be thought of as being carried out as one single interaction. In practice, they are implemented by processes that carry them out in a concurrent fashion. After formalising the intuitive semantics of grouped interactions, we prove that choreographic programs and their implementations are correct and deadlock-free by construction.

W4

Kokke, W., Montesi, F. and Peressotti, M. 2018. Taking Linear Logic Apart. *Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity-TLLA@FLoC 2018, Oxford, UK, 7-8 July 2018.* (2018), 90–103.

I6

Montesi, F. and Peressotti, M. 2018. Classical Transitions. *CoRR*. abs/1803.01049, (2018). DOI:10.48550/arXiv.1803.01049.

C6

Miculan, M. and Peressotti, M. 2017. Deciding weak weighted bisimulation. *Joint Proceedings of the 18th Italian Conference on Theoretical Computer Science and the 32nd Italian Conference on Computational Logic co-located with the 2017 IEEE International Workshop on Measurements and Networking (2017 IEEE M&N), Naples, Italy, September 26-28, 2017.* (2017), 126–137.

W3

Mansutti, A., Miculan, M. and Peressotti, M. 2017. Loose Graph Simulations. *Software Technologies: Applications and Foundations - STAF 2017 Collocated Workshops, Marburg, Germany, July 17-21, 2017, Revised Selected Papers* (2017), 109–126.

I5

Montesi, F. and Peressotti, M. 2017. Choreographies meet Communication Failures. *CoRR*. abs/1712.05465, (2017). DOI:10.48550/arXiv.1712.05465.

J4

De Nart, D., Degl’Innocenti, D. and Peressotti, M. 2016. Well-Stratified Linked Data for Well-Behaved Data Citation. *Bulletin of IEEE Technical Committee on Digital Libraries*. 12, 1 (2016), 16–26.

J3

Miculan, M. and Peressotti, M. 2016. Structural operational semantics for non-deterministic processes with quantitative aspects. *Theoretical Computer Science*. 655, (2016), 135–154. DOI:10.1016/j.tcs.2016.01.012.

The second contribution is a characterization of these systems as coalgebras of a class of functors, parametric in the weight structure. This result allows us to prove soundness and completeness of the WF-GSOS specification format, and that bisimilarities induced by these specifications are always congruences.

C5

Brengos, T. and Peressotti, M. 2016. A Uniform Framework for Timed Automata. *27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada* (2016), 26:1–26:15.

C4

Miculan, M. and Peressotti, M. 2016. On the Bisimulation Hierarchy of State-to-Function Transition Systems. *Proceedings of the 17th Italian Conference on Theoretical Computer Science, Lecce, Italy, September 7-9, 2016.* (2016), 88–102.

C3

De Nart, D., Degl’Innocenti, D., Peressotti, M. and Tasso, C. 2016. Stratifying Semantic Data for Citation and Trust: An Introduction to RDFDF. *Digital Libraries and Multimedia Archives - 12th Italian Research Conference on Digital Libraries, IRCDL 2016, Florence, Italy, February 4-5, 2016, Revised Selected Papers* (2016), 104–111.

I4

Miculan, M. and Peressotti, M. 2016. A Specification of Open Transactional Memory for Haskell. *CoRR*. abs/1602.05365, (2016). DOI:10.48550/arXiv.1602.05365.

I3

Peressotti, M. 2016. Endofunctors modelling higher-order behaviours. *CoRR*. abs/1602.06221, (2016). DOI:10.48550/arXiv.1602.06221.

J2

Brengos, T., Miculan, M. and Peressotti, M. 2015. Behavioural equivalences for coalgebras with unobservable moves. *Journal of Logical and Algebraic Methods in Programming*. 84, 6 (2015), 826–852. DOI:10.1016/j.jlamp.2015.09.002.

C2

Miculan, M., Peressotti, M. and Toneguzzo, A. 2015. Open Transactions on Shared Memory. *Coordination Models and Languages - 17th IFIP WG 6.1 International Conference, COORDINATION 2015, Held as Part of the 10th International Federated Conference on Distributed Computing Techniques, DisCoTec 2015, Grenoble, France, June 2-4, 2015, Proceedings* (2015), 213–229.

J1

Mansutti, A., Miculan, M. and Peressotti, M. 2014. Distributed execution of bigraphical reactive systems. *Electronic Communications of the EASST*. 71, (2014). DOI:10.14279/tuj.eceasst.71.994.

C1

Mansutti, A., Miculan, M. and Peressotti, M. 2014. Multi-agent Systems Design and Prototyping with Bigraphical Reactive Systems. *Distributed Applications and Interoperable Systems - 14th IFIP WG 6.1 International Conference, DAIS 2014, Held as Part of the 9th International Federated Conference on Distributed Computing Techniques, DisCoTec 2014, Berlin, Germany, June 3-5, 2014, Proceedings* (2014), 201–208.

This methodology allows the designer to benefit from the results and tools from the theory of BRS, especially in the requirement analysis and validation phases. Among other results, we mention behavioural equivalences, temporal/spatial logics, visual tools for editing, for simulation and for model checking, etc. Moreover, bigraphs can be naturally composed, thus allowing for modular design of MAS.

W2

Miculan, M. and Peressotti, M. 2014. GSOS for non-deterministic processes with quantitative aspects. *Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2014, Grenoble, France, 12-13 April 2014.* (2014), 17–33.

W1

Mansutti, A., Miculan, M. and Peressotti, M. 2014. Towards distributed bigraphical reactive systems. *Proc. GCM* (2014), 45.

I2

Miculan, M. and Peressotti, M. 2014. A CSP implementation of the bigraph embedding problem. *CoRR*. abs/1412.1042, (2014). DOI:10.48550/arXiv.1412.1042.

I1

Miculan, M. and Peressotti, M. 2013. Weak bisimulations for labelled transition systems weighted over semirings. *CoRR*. abs/1310.4106, (2013). DOI:10.48550/arXiv.1310.4106.