BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Unibo//DISI//BTFSS//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:Bologna seminar on Theory of software systems
X-WR-TIMEZONE:Europe/Rome
BEGIN:VEVENT
UID:2526-leblanc1@seminar.cs.unibo.it
DTSTAMP:20260731T220000Z
LAST-MODIFIED:20260731T220000Z
SEQUENCE:0
DTSTART;TZID=Europe/Rome:20260701T143000
DTEND;TZID=Europe/Rome:20260701T150000
SUMMARY:Seminar: Travis Leblanc\, “Interaction is invariant after all”
DESCRIPTION:Travis Leblanc\, ENS Paris-Saclay\n\nInteraction is invariant after all\n\nThe (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.
LOCATION:aula Seminari 2
END:VEVENT
BEGIN:VEVENT
UID:2526-capelli@seminar.cs.unibo.it
DTSTAMP:20260731T220000Z
LAST-MODIFIED:20260731T220000Z
SEQUENCE:0
DTSTART;TZID=Europe/Rome:20260701T140000
DTEND;TZID=Europe/Rome:20260701T143000
SUMMARY:Seminar: Marius Capelli\, “Model checking of higher order effectful programs”
DESCRIPTION:Marius Capelli\, ENS PSL\n\nModel checking of higher order effectful programs\n\nIn 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.
LOCATION:aula Seminari 2
END:VEVENT
BEGIN:VEVENT
UID:2526-lanese@seminar.cs.unibo.it
DTSTAMP:20260731T220000Z
LAST-MODIFIED:20260731T220000Z
SEQUENCE:0
DTSTART;TZID=Europe/Rome:20260624T140000
DTEND;TZID=Europe/Rome:20260624T150000
SUMMARY:Seminar: Ivan Lanese\, “On the Encodability of Reversible Process Calculi”
DESCRIPTION:Ivan Lanese\, Unibo\n\nOn the Encodability of Reversible Process Calculi\n\nReversibility\, 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.
LOCATION:aula Seminari 2
END:VEVENT
BEGIN:VEVENT
UID:2526-patrignani@seminar.cs.unibo.it
DTSTAMP:20260731T220000Z
LAST-MODIFIED:20260731T220000Z
SEQUENCE:0
DTSTART;TZID=Europe/Rome:20260616T110000
DTEND;TZID=Europe/Rome:20260616T120000
SUMMARY:Seminar: Marco Patrignani\, “Universal Composability is Robust Compilation”
DESCRIPTION:Marco Patrignani\, Università di Trento\n\nUniversal Composability is Robust Compilation\n\nThis talk discusses the relationship between two frameworks: universal composability (UC) and robust compilation (RC).\n\n            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.\n\n            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.\n\n            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.\n\n            This talk formally explores the benefits of this connection (focussing on perfect\, rather than computational UC).\n\n            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.
LOCATION:aula Seminari 2
END:VEVENT
BEGIN:VEVENT
UID:2526-peyrot@seminar.cs.unibo.it
DTSTAMP:20260731T220000Z
LAST-MODIFIED:20260731T220000Z
SEQUENCE:0
DTSTART;TZID=Europe/Rome:20260610T110000
DTEND;TZID=Europe/Rome:20260610T120000
SUMMARY:Seminar: Loïc Peyrot\, “Foundations for Liquid Haskell Through a Translation to Rocq”
DESCRIPTION:Loïc Peyrot\, IMDEA Software Institute\, Madrid\n\nFoundations for Liquid Haskell Through a Translation to Rocq\n\nLiquid 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.\n\n            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.\n\n            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.\n\n            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.
LOCATION:aula Busi
END:VEVENT
BEGIN:VEVENT
UID:2526-pizzo@seminar.cs.unibo.it
DTSTAMP:20260731T220000Z
LAST-MODIFIED:20260731T220000Z
SEQUENCE:0
DTSTART;TZID=Europe/Rome:20260603T110000
DTEND;TZID=Europe/Rome:20260603T120000
SUMMARY:Seminar: Nicolò Pizzo\, “A reversible Crumbling Abstract Machine for Plotkin's Call-by-Value”
DESCRIPTION:Nicolò Pizzo\, Unibo\n\nA reversible Crumbling Abstract Machine for Plotkin's Call-by-Value\n\nLandauer'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.\n\n            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.
LOCATION:aula Seminari 2
END:VEVENT
BEGIN:VEVENT
UID:2526-trogni@seminar.cs.unibo.it
DTSTAMP:20260731T220000Z
LAST-MODIFIED:20260731T220000Z
SEQUENCE:0
DTSTART;TZID=Europe/Rome:20260527T144500
DTEND;TZID=Europe/Rome:20260527T153000
SUMMARY:Seminar: Lea Trogni\, “Barbed Similarity for the π-Calculus in Beluga: A Case Study in Coinductive Reasoning”
DESCRIPTION:Lea Trogni\, Università di Milano\n\nBarbed Similarity for the π-Calculus in Beluga: A Case Study in Coinductive Reasoning\n\nThe 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.
LOCATION:aula Busi
END:VEVENT
BEGIN:VEVENT
UID:2526-cecilia@seminar.cs.unibo.it
DTSTAMP:20260731T220000Z
LAST-MODIFIED:20260731T220000Z
SEQUENCE:0
DTSTART;TZID=Europe/Rome:20260527T140000
DTEND;TZID=Europe/Rome:20260527T144500
SUMMARY:Seminar: Gabriele Cecilia\, “Formalizing reversible concurrent calculi in Beluga”
DESCRIPTION:Gabriele Cecilia\, Augusta University\n\nFormalizing reversible concurrent calculi in Beluga\n\nReversible 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. 
LOCATION:aula Busi
END:VEVENT
BEGIN:VEVENT
UID:2526-vergnani@seminar.cs.unibo.it
DTSTAMP:20260731T220000Z
LAST-MODIFIED:20260731T220000Z
SEQUENCE:0
DTSTART;TZID=Europe/Rome:20260506T140000
DTEND;TZID=Europe/Rome:20260506T150000
SUMMARY:Seminar: Mauro Vergnani\, “FaaSChalCore\, a Formal Choreographic Language for Function as a Service”
DESCRIPTION:Mauro Vergnani\, Unibo\n\nFaaSChalCore\, a Formal Choreographic Language for Function as a Service\n\nModern 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.
LOCATION:aula Busi
END:VEVENT
BEGIN:VEVENT
UID:2526-leblanc@seminar.cs.unibo.it
DTSTAMP:20260731T220000Z
LAST-MODIFIED:20260731T220000Z
SEQUENCE:0
DTSTART;TZID=Europe/Rome:20260429T140000
DTEND;TZID=Europe/Rome:20260429T150000
SUMMARY:Seminar: Travis Leblanc\, “A small extension to SIMREC”
DESCRIPTION:Travis Leblanc\, ENS Paris-Saclay\n\nA small extension to SIMREC\n\nSIMREC 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.
LOCATION:aula Busi
END:VEVENT
BEGIN:VEVENT
UID:2526-dallago@seminar.cs.unibo.it
DTSTAMP:20260731T220000Z
LAST-MODIFIED:20260731T220000Z
SEQUENCE:0
DTSTART;TZID=Europe/Rome:20260318T140000
DTEND;TZID=Europe/Rome:20260318T150000
SUMMARY:Seminar: Ugo Dal Lago\, “(Implicitly) Characterizing Probabilistic Polynomial Time as Used in Cryptography”
DESCRIPTION:Ugo Dal Lago\, Unibo\n\n(Implicitly) Characterizing Probabilistic Polynomial Time as Used in Cryptography\n\nWe 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.
LOCATION:aula Busi
END:VEVENT
BEGIN:VEVENT
UID:2526-quemerais@seminar.cs.unibo.it
DTSTAMP:20260731T220000Z
LAST-MODIFIED:20260731T220000Z
SEQUENCE:0
DTSTART;TZID=Europe/Rome:20260304T170000
DTEND;TZID=Europe/Rome:20260304T180000
SUMMARY:Seminar: Iwan Quémerais\, “First-order store and visibility in the π-calculus”
DESCRIPTION:Iwan Quémerais\, ENS de Lyon\n\nFirst-order store and visibility in the π-calculus\n\nThe π-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.
LOCATION:aula Seminari 2
END:VEVENT
BEGIN:VEVENT
UID:2526-gavazzo@seminar.cs.unibo.it
DTSTAMP:20260731T220000Z
LAST-MODIFIED:20260731T220000Z
SEQUENCE:0
DTSTART;TZID=Europe/Rome:20260218T110000
DTEND;TZID=Europe/Rome:20260218T120000
SUMMARY:Seminar: Francesco Gavazzo\, “Topics in Intensional Rewriting”
DESCRIPTION:Francesco Gavazzo\, Università di Padova\n\nTopics in Intensional Rewriting\n\nClassic 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.\n\n            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.\n\n            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.
LOCATION:aula Busi
END:VEVENT
BEGIN:VEVENT
UID:2526-cerda@seminar.cs.unibo.it
DTSTAMP:20260731T220000Z
LAST-MODIFIED:20260731T220000Z
SEQUENCE:0
DTSTART;TZID=Europe/Rome:20260204T110000
DTEND;TZID=Europe/Rome:20260204T120000
SUMMARY:Seminar: Rémy Cerda\, “Infinitary rewriting for the linear approximation of functional programs”
DESCRIPTION:Rémy Cerda\, Unibo\n\nInfinitary rewriting for the linear approximation of functional programs\n\nA 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.
LOCATION:aula Busi
END:VEVENT
BEGIN:VEVENT
UID:2526-lancelot@seminar.cs.unibo.it
DTSTAMP:20260731T220000Z
LAST-MODIFIED:20260731T220000Z
SEQUENCE:0
DTSTART;TZID=Europe/Rome:20260121T110000
DTEND;TZID=Europe/Rome:20260121T120000
SUMMARY:Seminar: Adrienne Lancelot\, “Interaction Equivalence”
DESCRIPTION:Adrienne Lancelot\, Unibo\n\nInteraction Equivalence\n\nContextual 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.\n\n            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.\n\n            See the paper.
LOCATION:aula Busi
END:VEVENT
BEGIN:VEVENT
UID:2526-issa@seminar.cs.unibo.it
DTSTAMP:20260731T220000Z
LAST-MODIFIED:20260731T220000Z
SEQUENCE:0
DTSTART;TZID=Europe/Rome:20251119T140000
DTEND;TZID=Europe/Rome:20251119T150000
SUMMARY:Seminar: Jad Issa\, “Static analysis of quantum/classical programs using hybrid path-sums”
DESCRIPTION:Jad Issa\, CEA Paris-Saclay\, Université de Lorraine\n\nStatic analysis of quantum/classical programs using hybrid path-sums\n\n
LOCATION:aula Busi
END:VEVENT
END:VCALENDAR