Monday, July 21, 2025

13:00-14:30. Lunch.

14:30-14:35. Introduction to WP3: Advanced Type Systems for interacting entities.
Davide Ancona (Università degli Studi di Genova)

14:35-15:00. Monadic Type-and-Effect Soundness.
Francesco Dagnino (Univeresità degli Studi di Genova)

Abstract. We introduce the abstract notions of monadic operational semantics, a small-step semantics where computational effects are modularly modeled by a monad, and type-and-effect system, including effect types whose interpretation lifts well-typedness to its monadic version. In this meta-theory, as usually done in the non-monadic case, we can express progress and subject reduction properties and provide a proof, given once and for all, that they imply soundness. The approach is illustrated on a lambda calculus with generic effects. We equip the calculus with an expressive type-and-effect system, and provide proofs of progress and subject reduction which are parametric on the interpretation of effect types. In this way, we obtain as instances many significant examples, such as checking exceptions, preventing/limiting non-determinism, constraining order/fairness of outputs on different locations. We also provide an extension with constructs to raise and handle computational effects, which can be instantiated to model different policies.

15:00-15:25. An Effectful Object Calculus.
Paola Giannini (Università degli Studi del Piemonte Orientale)

Abstract. We show how to smoothly incorporate in the object-oriented paradigm constructs to raise, compose, and handle effects in an arbitrary monad. The underlying pure calculus is meant to be a representative of the last generation of OO languages, and the effectful extension is manageable enough for ordinary programmers; notably, constructs to raise effects are just special methods. We equip the calculus with an expressive type-and-effect system, which, again by relying on standard features such as inheritance and generic types, allows a simple form of effect polymorphism. The soundness of the type-and-effect system is expressed and proved by a  recently  introduced technique, where the semantics is formalized by a one-step reduction relation from language expressions into monadic ones, so that it is enough to prove progress and subject reduction properties on this relation.

15:25-15:30. Questions and (Maybe) Answers, Discussion and Brainstorming.

15:30-16:00. Coffee Break.

16:00-16:05. Introduction to Keynote.
Walter Cazzola (Università degli Studi di Milano)

16:05-17:05. Typing Dynamic Languages with Set-Theoretic Types: The Case of Elixir (Keynote)
Giuseppe Castagna (Université Paris Cité)

Abstract. Dynamic programming languages like Elixir embrace programming patterns that challenge traditional type systems: non-uniform data structures, function overloading, and complex pattern matching. This talk presents our work on developing a static type system for Elixir based on set-theoretic types—a theoretical framework that naturally captures these dynamic programming idioms through union types, intersection types, and negation types.

We demonstrate how set-theoretic types solve fundamental typing challenges in Elixir without requiring any modification of existing code. The type system is the result of four years of collaboration with José Valim, the creator of Elixir, and his team, and is being gradually integrated into the Elixir compiler since version 1.17.

The talk illustrates how two decades of research in set-theoretic types culminate in a practical type system that scales to codebases with millions of lines of code, and demonstrates that static typing and dynamic programming styles can successfully coexist in a language used in production by companies like Discord, Pinterest, and PepsiCo.

Joint work with Guillaume Duboc and José Valim

17:05-17:30. Questions and (Maybe) Answers.

17:30-. TBD.

Tuesday, July 22, 2025

09:30-09:35. Resuming WP3: Advanced Type Systems for Interacting Entities.
Maurice ter Beek (ISTI-CNR Pisa)

09:35-10:00. Ain’t No Stopping Us Monitoring Now.
Francesco Dagnino (Università degli Studi di Genova)

Abstract. Not all properties are monitorable. This is a well-known fact, and it means there exist properties that cannot be fully verified at runtime. However, given a non-monitorable property, a monitor can still be synthesised, but it could end up in a state where no verdict will ever be concluded on the satisfaction (resp., violation) of the property. For this reason, non-monitorable properties are usually discarded. In this work, we carry out an in-depth analysis on monitorability, and how non-monitorable properties can still be partially verified. We present our theoretical results at a semantic level, without focusing on a specific formalism. Then, we show how our theory can be applied to achieve partial runtime verification of linear time properties expressed by concrete formalisms such as LTL.

10:05-10:25. On The Space Complexity of Partial Derivatives of Regular Expressions with Shuffle
Davide Ancona (Università degli Studi di Genova)

Abstract. Partial derivatives of regular expressions define an elegant algorithm for generating equivalent non-deterministic finite automata (NFA) with a limited number of states. Here we focus on runtime verification (RV) of simple properties expressible with regular expressions. In this case, words are finite traces of monitorable events forming the language’s alphabet, and the generated NFA may have an intractable number of states. This typically occurs when sub-traces of mutually independent events are allowed to interleave. To address this issue, regular expressions are extended with the shuffle operator. Exploiting partial derivatives enables a rewriting-based approach to RV, where only one derivative is stored at each step, avoiding the construction of an intractably large automaton. This raises the question of the space complexity of the largest generated partial derivative.  We study this problem w. r. t. two metrics and show that in both cases the results are invariant w. r. t. shuffle.

10:25-10:30. Questions and (Maybe) Answers, Discussion and Brainstorming.

10:30-11:00. Coffee Break.

11:00-11:05. Introduction to WP1: Models and Tools for Language Adaptation..
Walter Cazzola (Università degli Studi di Milano)

11:05-11:30. Overview and Roadmap of Team Automata: from Synchronous to Asynchronous Communication.
Maurice H. ter Beek (ISTI-CNR Pisa)

Abstract. Team Automata were introduced in GROUP'97 to model interacting component-based groupware systems, allowing multiple sending and receiving actions from concurrent automata to synchronise. Since then team automata have been studied and applied in many different contexts. In this talk, we first revisit the specific notion of synchronisation and composition of team automata and briefly compare them with other coordination models, namely Reo, BIP, Contract Automata, Choreography Automata, and Multi-Party Session Types. We then give an overview of several aspects that have recently been investigated for team automata and related models, namely communication safety (can receptiveness and responsiveness be guaranteed?), realisability (can a global model be decomposed into local components?), variability (can composition and communication safety be lifted to family models?), and tool support (what has been implemented?). After this snapshot of recent research on team automata, we delineate a roadmap for future research on asynchronous communication in team automata and how this impacts communication properties and realisability.

11:30-11:55. Human-Centred Evaluations of Software Representations: Requirements, Formal Notations, and Tools.
Giovanna Broccia (ISTI-CNR Pisa)

Abstract. This presentation explores a human-centred perspective on the evaluation of software representations, spanning formal notations, language workbenches, and requirements artifacts. Through a series of empirical studies, we investigate the understandability and user acceptance of Attack-Defense Trees (ADTs), the understandability, user acceptance, and relationship with working memory capacity in language workbenches such as Neverlang, and the impact of cognitive abilities on the effectiveness of UML diagrams in requirements inspection. The findings underscore the dual importance of technical accuracy and user-centred design, revealing that while formal notations like ADTs are generally well-understood and accepted, tools such as language workbenches present challenges in ease of use. Additionally, the usefulness of visual representations like UML varies significantly with users' cognitive profiles, particularly working memory and mental rotation abilities. These results emphasise the need to balance formality and usability, and to tailor software engineering tools and practices to diverse user characteristics.

11:55-12:20. When Contrastive Learners are Semantic Learners.
Francesco Bertolotti (Università degli Studi di Milano)

Abstract. In this work, we explore the definition of semantic equivalence to establish a connection between contrastive tasks and their downstream counterparts. Specifically, we investigate when a contrastive dataset can learn representations that encode formal semantic equivalence relations for a specific downstream task. In our analysis, we recover a surprising hypothesis resembling the distributional one---dubbed distributional alignment hypothesis. Under this assumption, we demonstrate that the optimal model for simple contrastive learning procedure must generate representations that encode formal semantic equivalence relations for the downstream task. We further show that the optimal embedding must be a quasi-isometric embedding between the semantic space and the embedding space, indicating a deep connection between the two spaces. Finally, we support the theory with a series of experiments designed to test the presented intuitions.

Joint work with Walter Cazzola

12:20-12:30. Questions and (Maybe) Answers, Discussion and Brainstorming.

12:30-14:00. Lunch.

14:00-14:05. Resuming WP1: Models and Tools for Language Adaptation.
Davide Ancona (Università degli Studi di Genova)

14:05-14:30. Maude (And Petri Nets): A Framework for the Analysis of Adaptive Concurrent Systems.
Lorenzo Capra (Università degli Studi di Milano)

Abstract. Modern distributed systems need adaptation and self-reconfiguration to handle dynamic environments while controlling costs, necessitating comprehensive formal models. Traditional methods like Petri nets, Process Algebras, and Automata struggle with specifying dynamic system changes and their impacts. This has led to the creation of extended models such as the Pi calculus, the Ambient calculus, and the Nets-within-Nets paradigm, although they often lack proper analysis techniques and tools.

In this presentation, we explore the potential of using Maude, a purely declarative language with sound Rewriting Logic semantics, as a unifying framework for the analysis of adaptive concurrent systems. Specifically, we will discuss recent integral implementations of dynamic Petri nets in Maude, including modular rewritable Petri nets and algebraic Petri nets with active tokens, as well as recent advancements in employing Maude for stochastic analysis.

Joint work with Michael Köhler-Bußmeier

14:30-14:55. Code Less to Code More.
Luca Favalli (Università degli Studi di Milano)

Abstract. Developing editing support for $mathcal{L}$ languages in $mathcal{E}$ editors is complex and time-consuming. Some languages do not provide dedicated editors, while others offer a single native editor. The language server protocol (LSP) reduces the language-editor combinations $mathcal{L} times mathcal{E}$ to $mathcal{L} + mathcal{E}$, where a single language server communicates with editors via LSP plugins. However, overlapping implementations of linguistic components remain an issue. Existing language workbenches struggle with modularity, reusability, and leveraging type systems for language server generation. In this work, we propose: (i) Typelang, a family of domain-specific languages for modular, composable, and reusable type system implementation, (ii) a modular language server generation process, producing servers for languages built in a modular workbench, (iii) the variant-oriented programming paradigm and a cross-artifact coordination layer to manage interdependent software variants, and (iv) an LSP plugin generator, reducing $mathcal{E}$ to $mathbf{1}$ by automating plugin creation for multiple editors. To simplify editing support for language families, each language artifact integrates its own Typelang variant, used to generate language servers. This reduces combinations to T×1, where T=L represents the number of type systems. Further reuse of language artifacts across languages lowers this to N×1, where N«T, representing unique type systems. We implement Typelang in Neverlang, generating language servers for each artifact and LSP plugins for three editors. Empirical evaluation shows a 93.48% reduction in characters needed for type system implementation and 100% automation of LSP plugin generation, significantly lowering effort for editing support in language families, especially when artifacts are reused.

Joint work with Federico Bruzzone e Luca Favalli

14:55-15:20. SHAC++: A Neural Network to Rule All Differentiable Simulators.
Francesco Bertolotti (Università degli Studi di Milano)

Abstract. Reinforcement learning (RL) algorithms show promise in robotics and multi-agent systems but often suffer from low sample efficiency. While methods like SHAC leverage differentiable simulators to improve efficiency, they are limited to specific settings: they require fully differentiable environments (including transition and reward functions) and have primarily been demonstrated in single-agent scenarios. To overcome these limitations, we introduce textsc{SHAC++}, a novel framework inspired by SHAC@. textsc{SHAC++} removes the need for differentiable simulator components by using neural networks to approximate the required gradients, training these networks alongside the standard policy and value networks. This allows the core SHAC approach to be applied in both non-differentiable and multi-agent environments. We evaluate textsc{SHAC++} on challenging multi-agent tasks from the VMAS suite, comparing it against SHAC (where applicable) and PPO, a standard algorithm for non-differentiable settings. Our results demonstrate that textsc{SHAC++} significantly outperforms PPO in both single- and multi-agent scenarios. Furthermore, in differentiable environments where SHAC operates, textsc{SHAC++} achieves comparable performance despite lacking direct access to simulator gradients, thus successfully extending SHAC's benefits to a broader class of problems.

Joint work with Gianluca Aguzzi, Walter Cazzola and Mirko Viroli

15:20-15:30. Questions and (Maybe) Answers, Discussion and Brainstorming.

15:30-16:00. Coffee Break.

16:00-16:05. Introduction to Keynote.
Walter Cazzola (Università degli Studi di Milano)

16:05-17:05. My Software Abstraction Is Better Than Yours, Objectively! (Keynote)
Mirko Viroli (Univcersità degli Studi di Bologna)

Abstract. Every researcher in the area of programming languages, software engineering, or theoretical computer science, at least once has come up with some new programming abstraction (construct, library, framework) claiming it is a good match at least for some class of problems. Finding true scientific evidence for one such claim is not easy, though. How can we show that some developer/engineer will, with a certain amount of training, actually take advantage of our new abstraction? How can we measure the trade-off between learning curve and productivity boost, objectively? To this end, LLMs can play an important role, for they can inject objectiveness and reproducibility in the task of "training to an abstraction and measure corresponding increase of productivity".

In this talk, I'll focus on a computing abstraction I've been developing for the past 10 years: aggregate computing. It allows you to express in a purely declarative way increasingly complex distributed asynchronous computations situated in space, abstracting away several network and communication concerns, and capturing key self-adaptation properties formally. Applications areas span distributed IoT, sensor networks, and swarms.

I'll report on the current state of our research devoted to training LLMs on what aggregate computing can do, seeking help in writing new libraries and systems.

17:05-17:30. Questions and (Maybe) Answers.

20:30. Social Dinner at Osteria le Colonne

Wednesday, July 23, 2025

09:30-09:35. Introduction to WP2: Interaction for interoperability and adaptation and WP4: Application to IoT SW development.
Maurice ter Beek (ISTI-CNR Pisa)

09:35-10:00. TBD.
Federico Bergenti (Univeirstà degli Studi di Parma)

Abstract. TBD

Joint work with TBD

10:00-10:25. An Ecosystem to Develop Multi-Agent Systems in Real-World IoT Applications.
Fabrizio Messina (Università degli Studi di Catania)

Abstract. Software agents and multi-agent systems are critical components in the development of distributed autonomous systems, as they exhibit a wide range of "intelligence", from reactive behaviours to advanced reasoning and planning. Integrating these capabilities into multi-agent systems enables distributed artificial intelligence, a programming paradigm in which autonomous entities work together efficiently across a network to achieve shared goals. Another important aspect we consider in this work is represented by the disruptive impact of 5G technology, which is moving computation to the edge of the network. As a result of this shift, embedded devices with microcontrollers – which are renowned for their low power consumption and limited computing power – have proliferated. This paradigm fits in well with the small cooperating entities scattered across the network in this situation but, at the same time, it is difficult to provide agent platforms for embedded devices, though. Indeed, the most recent state-of-the-art MAS platforms, which are primarily Java-based, raise issues with microcontroller speed and memory overhead. To achieve this goal, we designed and implemented an ecosystem, entirely written in C++, to create multi-agent systems in an actual Internet of Things setting. Our ecosystem is compounded by Democle, a logic/declarative agent programming framework, and Hermes, a unified wireless network interface, both specifically created for embedded systems. In this paper, we describe our ecosystem’s functionality, architecture, and benefits of use. In addition, we provide a case study and a few experiments to prove how our platform works and its efficiency in terms of overhead.

10:25-10:50. TBD.
Stefania Monica (Università degli Studi di Modena e Reggio Emilia)

Abstract. TBD.

10:50-11:00. Questions and (Maybe) Answers, Discussion and Brainstorming.

11:00-11:30. Coffee Break.

11:30-13:00. Discussion on What's Next about T-LADIES.

13:00-13:00. Closing.
Walter Cazzola (Università degli Studi di Milano)

13:00-14:30. Lunch.