Bologna seminar on Theory of software systems

Upcoming talks

Wed 24 Jun 2026, 14:00, aula Seminari 2
Ivan Lanese (Unibo), “On the Encodability of Reversible Process Calculi”
Abstract. Reversibility, allowing one to execute a program not only forwards as usual, but also backwards, has emerged as a main concept in computing, with applications ranging from debugging and fault tolerance to biological and quantum systems. CCSK, a reversible extension of CCS, is a paradigmatic model of reversible concurrent computation. In this paper, we investigate the encodability of CCSK into classical forward-only concurrent models. We establish a separation theorem showing that there is no basic, success-sensitive encoding of CCSK into CCS or the π-calculus, highlighting the strong impact of reversibility on the expressive power. We then present an encoding of CCSK processes with only top-level parallel composition into the internal π-calculus, correct up to strong bisimilarity. We also identify a fundamental limitation: no parallel-preserving encoding of CCSK (with arbitrary parallel composition) into the π-calculus can be correct up to strong bisimilarity. Finally, we provide a parallel-preserving encoding correct under a weaker behavioural correspondence: weak mutual simulation. Our findings extend the literature of encodability results to reversible process calculi.
Wed 1 Jul 2026, 14:00, aula Seminari 2
Marius Capelli (ENS PSL), “Model checking of higher order effectful programs”
Abstract. In the setting of monomorphic effects handlers the reachabily property is known to be undecidable. We propose a type system to restrict it to a decidable set of programs, and compare it to other existing solutions.
Wed 1 Jul 2026, 14:30, aula Seminari 2
Travis Leblanc (ENS Paris-Saclay), “Interaction is invariant after all”
Abstract. The (lambda) Interaction Abstract Machine (IAM) is an abstract machine for the untyped lambda calculus inspired by Girard's Geometry of Interaction. It was thought by the literature to be time inefficient but space efficient. We show, at the contrary, that the lambda IAM is an invariant cost model for time, and argue for its space inefficiency.

Past talks

Tue 16 Jun 2026, 11:00, aula Seminari 2
Marco Patrignani (Università di Trento), “Universal Composability is Robust Compilation”
Abstract. This talk discusses the relationship between two frameworks: universal composability (UC) and robust compilation (RC).
In cryptography, UC is a framework for the specification and analysis of cryptographic protocols with a strong compositionality guarantee: UC protocols remain secure even when composed with other protocols.
In programming language security, RC is a novel framework for determining secure compilation by proving whether compiled programs are as secure as their source-level counterparts no matter what target-level code they interact with.
Presently, these disciplines are studied in isolation, though we argue that there is a deep connection between them and exploring this connection will benefit both research fields.
This talk formally explores the benefits of this connection (focussing on perfect, rather than computational UC).
This connection lays the groundwork towards a better and deeper understanding of both UC and RC, and the benefits we showcase from this connection provide evidence of scalable mechanised proofs for UC.
Wed 10 Jun 2026, 11:00, aula Busi
Loïc Peyrot (IMDEA Software Institute, Madrid), “Foundations for Liquid Haskell Through a Translation to Rocq”
Abstract. Liquid Haskell (LH) is a plugin for the Haskell compiler that enables augmenting the specifications of types with refinement: logical predicates (written in Haskell) restricting the domain of the types. Specifications are automatically checked by an SMT solver, thus offering lightweight specification directly within an industrial-strength language.
But several unsoundness bugs are unveiled every year, thus raising the question of trust in the verification and the necessity for formalized semantics of LH. Giving foundations is complicated by the interaction between two semantic levels in the language: the computational one and the logical one (of predicates). While the first one is better understood, no formal accounts of the logical component has been proposed for a refinement type system, due to its complexity and reliance on the external SMT solver.
Our approach is to give a semantics in terms of a translation to a depently-typed system, namely Rocq. This way, both the computational and logical parts are translated in the same language, with a well-understood semantics. We will see in particular how the dual semantics of LH objects must be reflected in the translation.
The translation is implemented in Haskell and comes with a Rocq library including powerful proof automation replacing the SMT solver. Thus, on the practical level, this tool serves as a certificate checker for the supported subset of LH.
Wed 3 Jun 2026, 11:00, aula Seminari 2
Nicolò Pizzo (Unibo), “A reversible Crumbling Abstract Machine for Plotkin's Call-by-Value”
Abstract. Landauer's embeddings enable the reversibility of each computational step for non-reversible programming languages, augmenting each intermediate state with enough data to reconstruct the previous state.
An interesting research question is therefore to try to reduce the required space overhead: in this talk I will present a compact Landauer’s embedding for Plotkin’s call-by-value calculus (CbV), implemented via an Abstract Crumbling Machine, a reduction machine for λ-calculus where the sequence of explicit substitutions in the environment encode both the evaluation order and the reduction context. Therefore, crumbling machines are both extremely parsimonious in data structures, and do not need to be modified to work on different reduction orders.
Wed 27 May 2026, 14:45, aula Busi
Lea Trogni (Università di Milano), “Barbed Similarity for the π-Calculus in Beluga: A Case Study in Coinductive Reasoning”
Abstract. The Concurrent Calculi Formalization Benchmark is a set of benchmark problems designed to evaluate the formalization of models of concurrent systems. In particular, its third challenge investigates the mechanization of coinductive reasoning, taking the context lemma for barbed congruence in the π-calculus as a case study. We provide a solution to this challenge in Beluga, a proof assistant that features higher-order abstract syntax (HOAS), copattern-based coinduction, and built-in simultaneous substitutions. To capture infinite behaviour, we consider a fragment of the π-calculus with replication. Our development demonstrates the effectiveness of HOAS even in the presence of contexts that are not α-convertible, and includes formal proofs of some compatibility properties.
Wed 27 May 2026, 14:00, aula Busi
Gabriele Cecilia (Augusta University), “Formalizing reversible concurrent calculi in Beluga”
Abstract. Reversible concurrent calculi are abstract models of concurrent systems in which any action can potentially be undone. Over the last few decades, different formalisms have been developed and their mathematical properties have been explored; however, until recently, none had been machine-checked in a proof assistant. This talk presents an overview of the first formalization in the proof assistant Beluga of two reversible extensions of the Calculus of Communicating Systems (CCS), namely CCS with Keys (CCSK) and CCS with Keys and Proof labels (CCSKP). The formalized results include the existence of a bijection between the transition systems of the two calculi, the proof that they satisfy the core axioms and properties of the axiomatic approach to reversibility, and several properties of the relations of dependence, independence and connectivity of proof labels. As is often the case with formalizations, the encoding introduces adjustments to the informal proofs and makes explicit details which were previously only sketched, some of which reveal to be less straightforward than initially assumed.
Wed 6 May 2026, 14:00, aula Busi
Mauro Vergnani (Unibo), “FaaSChalCore, a Formal Choreographic Language for Function as a Service”
Abstract. Modern computing relies more than ever on two aspects: concurrency, the performance of multiple tasks at the same time; and distribution, the usage of components located on different communicating devices. This is due to the rising importance of the World Wide Web, the Internet of Things, and telecommunications, and due to the rising popularity of edge computing and cloud computing, all of which lead to larger computer networks. Cloud computing in particular is one of the main environments where distributed systems run, since it allows for greater scalability and easier management of resources. One of the main design approaches used with cloud computing is serverless computing with Function as a Service, which consists of defining functions with specific triggers, letting the cloud provider handle their instantiation when they are triggered. For these reasons we have defined FaaSChalCore, a formal choreographic language tailored for Function as a Service, which allows the programmer to define the behaviour of the entire system in a single program. In this seminar we will go over the defining elements of the language, the design decisions behind them, and the formal properties that FaaSChalCore possesses, with a focus on how the language handles serverless functions.
Wed 29 Apr 2026, 14:00, aula Busi
Travis Leblanc (ENS Paris-Saclay), “A small extension to SIMREC” (url)
Abstract. SIMREC is a language proven to be sound and complete for PTIME by Dal Lago and Avanzini. The main features are algebraic data types and mutually recursive functions. We will see how it works and present a small extension to the language as well as some non-trivial examples written in the language.
Wed 18 Mar 2026, 14:00, aula Busi
Ugo Dal Lago (Unibo), “(Implicitly) Characterizing Probabilistic Polynomial Time as Used in Cryptography”
Abstract. We show that a recently introduced lambda-calculus for randomized computation, called lambdaBLL, can accurately capture the notions of first- and second-order polytime computations used in cryptographic definitions and proofs. These results, spelled out in the style of so-called implicit computational complexity, imply that lambdaBLL is sufficiently powerful to express experiments and adversaries as used in cryptography, and that reductions, when formulated within the calculus, are guaranteed to be complexity-preserving. Remarkably, while polynomial-time soundness holds for the full calculus, polynomial-time completeness already follows in presence of a minimal and finite set of basic functions.
Wed 4 Mar 2026, 17:00, aula Seminari 2
Iwan Quémerais (ENS de Lyon), “First-order store and visibility in the π-calculus”
Abstract. The π-calculus is the paradigmatical name-passing calculus. While being purely name-passing, it allows the representation of higher-order functions and store. In this talk I will explain how π-calculus processes can be controlled so that computations can only involve storage of first-order values. The discipline is enforced by a type system that is based on the notion of visibility, coming from game semantics. I will discuss the impact of visibility on the behavioural theory and present a characterisations of barbed equivalence, based on a variant of labelled bisimilarity, in the case where computation is sequential.
Wed 18 Feb 2026, 11:00, aula Busi
Francesco Gavazzo (Università di Padova), “Topics in Intensional Rewriting”
Abstract. Classic rewriting theory studies the computational content of syntactic objects as generated by transformational rules, generically referred to as reductions. Many such objects---such as programs, types, and proofs---however, exhibit operational behaviours that significantly go beyond pure computation. Examples of such behaviours include interaction with the environment, resource consumption, and, more generally, computational effects and coeffects.
Accounting for these intensional behaviours requires enriching the classic notion of reduction in nontrivial ways, yielding to intensional notions of reduction, such as monadic and quantitative reductions, along with the corresponding theories of rewriting.
In this talk, after introducing the aforementioned notions of intensional rewriting, I will give an overview of various open problems and research directions in these areas, hinting at potential solutions and developments where possible. While the literature on rewriting tends to privilege syntactic approaches (and, more rarely, geometrical ones), I will argue that an algebraic approach to reduction naturally emerges as a unifying pattern behind different forms of rewriting.
Wed 4 Feb 2026, 11:00, aula Busi
Rémy Cerda (Unibo), “Infinitary rewriting for the linear approximation of functional programs” (slides)
Abstract. A standard technique in λ-calculus is continuous program approximation, where the semantics of a program is described as a limit of finite approximants. It can be refined into a linear approximation where an operation of Taylor expansion takes a program to a power series of finite approximants. In this talk, I rebuild this longstanding line of work using what can arguably be presented as the “missing ingredient”, infinitary rewriting. Depending on the time remaining and the wishes of the audience, I will show a few other interesting results or questions around the lines of an infinitary Curry-Howard correspondence.
Wed 21 Jan 2026, 11:00, aula Busi
Adrienne Lancelot (Unibo), “Interaction Equivalence” (slides)
Abstract. Contextual equivalence is the de facto standard notion of program equivalence. A key theorem is that contextual equivalence is an equational theory. Making contextual equivalence more intensional, for example taking into account the time cost of the computation, seems a natural refinement. Such a change, however, does not induce an equational theory, for an apparently essential reason: cost is not invariant under reduction.
In the paradigmatic case of the untyped λ-calculus, we introduce interaction equivalence. Inspired by game semantics, we observe the number of interaction steps between terms and contexts but — crucially — ignore their own internal steps. We prove that interaction equivalence is an equational theory and we characterize it as B, the well-known theory induced by Böhm tree equality. Ours is the first observational characterization of B obtained without enriching the discriminating power of contexts with extra features such as non-determinism. To prove our results, we develop interaction-based refinements of the Böhm-out technique and of intersection types.
See the paper.
Wed 19 Nov 2025, 14:00, aula Busi
Jad Issa (CEA Paris-Saclay, Université de Lorraine), “Static analysis of quantum/classical programs using hybrid path-sums”