Bologna seminar on Theory of software systems

Upcoming talks

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 3 Jun 2026, 14:00, aula Busi
Nicolò Pizzo (Unibo), TBA
Tue 16 Jun 2026, 11:00, aula Busi (unusual day and time!)
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.

Past talks

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”