19 citations · 96 across the 34 of their papers we have counts for
42 papers
Accompanist: A Runtime for Resilient Choreographic Programming
Viktor Strate Kløvedal, Dan Plyukhin, Marco Peressotti +1
In service-oriented architecture, services coordinate in one of two ways: directly, using point-to-point communication, or indirectly, through an intermediary called the orchestrat…
Type-Based Enforcement of Non-Interference for Choreographic Programming
Marco Bertoni, Saverio Giallorenzo, Marco Peressotti
Choreographies describe distributed protocols from a global viewpoint, enabling correct-by-construction synthesis of local behaviours. We develop a policy-parametric type system th…
Hennessy-Milner Logic in CSLib, the Lean Computer Science Library
Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker
We present a library-level formalisation of Hennessy-Milner Logic (HML) - a foundational logic for labelled transition systems (LTSs) - for the Lean Computer Science Library (CSLib…
A Conceptual Framework for API Refactoring in Enterprise Application Architectures
Fabrizio Montesi, Marco Peressotti, Valentino Picotti +1
Enterprise applications are often built as service-oriented architectures, where the individual services are designed to perform specific functions and interact with each other by…
On Propositional Dynamic Logic and Concurrency
Matteo Acclavio, Fabrizio Montesi, Marco Peressotti
Dynamic logic is a powerful approach to reasoning about programs and their executions, obtained by extending classical logic with modalities that can express program executions as…
Ozone: Fully Out-of-Order Choreographies
Dan Plyukhin, Marco Peressotti, Fabrizio Montesi
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 genera…
Reasoning about Choreographic Programs
Luís Cruz-Filipe, Eva Graversen, Fabrizio Montesi +1
Choreographic programming is a paradigm where a concurrent or distributed system is developed in a top-down fashion. Programs, called choreographies, detail the desired interaction…
A Formal Theory of Choreographic Programming
Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti
Choreographic programming is a paradigm for writing coordination plans for distributed systems from a global point of view, from which correct-by-construction decentralised impleme…
Model-Driven Generation of Microservice Interfaces: From LEMMA Domain Models to Jolie APIs
Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti +1
We formally define and implement a translation from domain models in the LEMMA modelling framework to microservice APIs in the Jolie programming language. Our tool enables a softwa…
Functional Choreographic Programming
Luís Cruz-Filipe, Eva Graversen, Lovro Lugović +2
Choreographic programming is an emerging programming paradigm for concurrent and distributed systems, whereby developers write the communications that should be enacted and then a…
Linear Logic, the -calculus, and their Metatheory: A Recipe for Proofs as Processes
Fabrizio Montesi, Marco Peressotti
Initiated by Abramsky [1994], the Proofs as Processes agenda is to establish a solid foundation for the study of concurrent languages, by researching the connection between linear…
On the Monitorability of Session Types, in Theory and Practice (Extended Version)
Christian Batrolo Burlò, Adrian Francalanza, Alceste Scalas
In concurrent and distributed systems, software components are expected to communicate according to predetermined protocols and APIs - and if a component does not observe them, the…
Jolie & LEMMA: Model-Driven Engineering and Programming Languages Meet on Microservices
Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti +2
In the field of microservices, Model-Driven Engineering has emerged as a powerful methodology for architectural design, and new programming languages have introduced language abstr…
Sliceable Monolith: Monolith First, Microservices Later
Fabrizio Montesi, Marco Peressotti, Valentino Picotti
We propose Sliceable Monolith, a new methodology for developing microservice architectures and perform their integration testing by leveraging most of the simplicity of a monolith:…
Formalising a Turing-Complete Choreographic Language in Coq
Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti
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…
Certifying Choreography Compilation
Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti
Choreographic programming is a paradigm for developing concurrent and distributed systems, where programs are choreographies that define, from a global viewpoint, the computations…
Software Transactional Memory with Interactions
Marino Miculan, Marco Peressotti
Software Transactional memory (STM) is an emerging abstraction for concurrent programming alternative to lock-based synchronizations. Most STM models admit only isolated transactio…
Choral: Object-Oriented Choreographic Programming
Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti
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 t…
A CSP implementation of the directed bigraph embedding problem
Alessio Chiapperini, Marino Miculan, Marco Peressotti
Directed bigraphs are a meta-model which generalises Milner's bigraphs by taking into account the request flow between controls and names. A key problem about these bigraphs is tha…
Towards a Formal Model for Composable Container Systems
Fabio Burco, Marino Miculan, Marco Peressotti
In modern cloud-based architectures, containers play a central role: they provide powerful isolation mechanisms such that developers can focus on the logic and dependencies of appl…
A Graph-Based Tool to Embed the π-Calculus into a Computational DPO Framework
Jakob Lykke Andersen, Marc Hellmuth, Daniel Merkle +2
Graph transformation approaches have been successfully used to analyse and design chemical and biological systems. Here we build on top of a DPO framework, in which molecules are m…
Two modes of recognition: algebra, coalgebra, and languages
Tomasz Brengos, Marco Peressotti
The aim of the paper is to build a connection between two approaches towards categorical language theory: the coalgebraic and algebraic language theory for monads. For a pair of mo…
No more, no less - A formal model for serverless computing
Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese +3
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 appl…
Taking Linear Logic Apart
Wen Kokke, Fabrizio Montesi, Marco Peressotti
Process calculi based on logic, such as DILL and CP, provide a foundation for deadlock-free concurrent programming. However, in previous work, there is a mismatch between the ru…