Rémi Di Guardia

Quantum Bayesian networks provide a mathematical formalism to describe causal relations, to analyse correlations, and to predict the probabilities of measurement outcomes, in systems involving both classical and quantum data. They generalize Pearl’s Bayesian networks—prominent graphical models for classical probabilistic reasoning and inference.
The goal of this paper is to bring compositional principles and a typing discipline into this setting. A key feature of our compositional semantics is that when all causes are classical, it coincides with the standard factor-based semantics of Bayesian networks, while in the purely quantum case it reduces to tensor networks. We then propose a typed formalism based on linear logic proof-nets, where types ensure well-behaved composition of systems, and which we prove sound and complete with respect to quantum Bayesian networks.

Proofs in a logic are usually considered (at least) up to cut-elimination. This is the case in linear logic, that also has another equivalence relation on proofs: rule commutation. We prove these two notions coincide in second-order linear logic and many of its fragments. Moreover, we show that equality up to rule commutation is undecidable in propositional linear logic—and so is equality up to cut-elimination.

Few results are known on uniform interpolation for linear logic, the main one being that Multiplicative-Additive Linear Logic has the uniform interpolation property (and so does its intuitionistic variant) [Alizadeh, Derakhshan, Ono 2014]. We present a simple counter-example to this property for formulas of Multiplicative-Exponential Linear Logic (and its intuitionistic variant).

Quantum Bayesian networks provide a mathematical formalism to describe causal relations, to analyse correlations, and to predict the probabilities of measurement outcomes, in systems involving both classical and quantum data. They generalize Pearl’s Bayesian networks—prominent graphical models for classical probabilistic reasoning and inference.
This extended abstract reports on work which brings compositional principles and a typing discipline into this setting. A key feature of our compositional semantics is that when all causes are classical, it coincides with the standard factor-based semantics of Bayesian networks, while in the purely quantum case it reduces to tensor networks. We then propose a typed formalism based on linear logic proof-nets, where types ensure well-behaved composition of systems.

Quantum Bayesian networks from [Henson, Lal, Pusey] provide a mathematical formalism to describe causal relations, to analyse correlations, and to predict the probabilities of measurement outcomes, in systems involving both classical and quantum data. They generalize Pearl's Bayesian networks---prominent graphical models for classical probabilistic reasoning and inference.
Our goal is to bring compositional principles and a typing discipline into this setting. A key feature of our compositional semantics is that when all causes are classical, it coincides with the standard factor-based semantics of Bayesian networks, while in the purely quantum case it reduces to tensor networks. We then propose a typed formalism based on linear logic proof-nets, where types ensure well-behaved composition of systems, and which we prove sound and complete with respect to quantum Bayesian networks.

A general task of quantum theory is to predict the probabilities of measurement outcomes for a given system. In this sense, it can be framed as a problem of probabilistic inference over models involving both classical and quantum data. In the classical setting, Pearl’s Bayesian networks are a prominent graphical model to describe probability distributions in a compact way. They capture classical causality and enable efficient inference algorithms. The generalization of Bayesian networks to include quantum causes is an active line of research. We revisit some works in this line, specifically [Wood and Spekkens 2012, Leifer and Spekkens 2013, Henson Lal Pusey 2014], by bringing methods and concepts from proof-theory and the semantics of programming languages, which allows for typing and compositional reasoning. We propose a model which neatly encompasses both classical and quantum causal scenarios, while enabling the graphical methods typical of Bayesian networks. This allows in particular to study conditional independence (no-signaling) between random variables in a probability distribution, regardless of the fact that some of the causes are quantum. Our semantics adapts the one of [Selinger 2004] in order to obtain the following feature: when all causes are classical, the mathematical structure is the standard factors-based semantics of Bayesian networks, whereas in the fully quantum case it yields standard tensor-networks. Our graphical syntax, that is based on Linear Logic, is typed which allows for the composition of systems to be well-behaved.

This talk considers the identity of proofs: when are two proofs equal? Generally, syntactic equality is too constrained, and one wants to identify proofs (at least) up to cut-elimination - which is similar to identifying λ-terms up to β-reduction. This is the case, for instance, when considering a denotational model or when studying isomorphisms. We begin by giving intuitions for this problem in simply typed λ-calculus, where it is easily solved thanks to strong normalization and confluence of β-reduction. Then, we see which problems arise when trying to mimic this reasoning in Linear Logic. The main difficulty is that cut-elimination is only confluent up to an equivalence relation known as rule commutations, a result that is not easy to prove. In particular, it involves strong normalization of cut-elimination (and more), which is a known but far from trivial result in linear logic. We conclude by showing that knowing whether two given proofs are equal up to rule commutations, or not, is undecidable. This entails that one cannot decide whether two proofs of linear logic are equal up to cut-elimination.

Bayesian Networks are a graphical syntax describing probability distributions compactly by following dependencies of variables. I will present the correspondence between these Bayesian Networks and Proof Nets, a graphical syntax for proofs in linear logic. Uses of such a correspondence are giving a proof-theoretical account of Bayesian inference (in the spirit of the Curry-Howard correspondence), and exploiting the expressivity of Proof Nets to get compositional graphical methods where each intermediate graph is associated to a probability distribution.
(Join work with Thomas Ehrhard and Claudia Faggian.)

This talk studies the identity of proofs: when are two proofs equal? Generally, syntactic equality is too constraint, and one wants to (at least) identify proofs up to cut-elimination - which is similar to identifying λ-terms up to β-reduction. We begin by giving intuitions for this problem in simply typed λ-calculus, where it is easily solved thanks to strong normalization and confluence of β-reduction. Then, we see which problems arise when trying to mimic this reasoning in Linear Logic. The main difficulty is that cut-elimination is only confluent up to an equivalence relation known as rule commutations, which is not easy to prove. We conclude by showing that knowing whether two given proofs are equal up to rule commutations, or not, is undecidable.

Cut-elimination is a rewriting system defined in many logics, which has been widely studied. In general, a major result is to prove its weak normalization, which implies a provable formula always admits a cut-free proof. From this, various results can be more easily deduced: for instance that there is no proof of false. However, the reverse procedure - that we call cut-expansion - has been much less studied even though it is also useful! A goal here is the following: given a proof π with many cuts, can we find a proof π' with exactly one cut at its root and that reduces to π? Such a result has two applications. First, it allows to find a Craig's interpolant in the spirit of [Sau25,FOS25]. It is also useful in the case of a denotational semantic: while it is often clear how to interpret a single cut-rule between two proofs, it may not be the case for two proofs linked by "a bunch" of cut-rules - this problem was encountered e.g. in [EFP24]. We will present a very simple proof on how to apply cut-expansion steps to obtain only one cut-rule from a proof with many cut-rules in Multiplicative Linear Logic. We do so in the proof-net syntax as the proof is really easy to intuit in this formalism. We then use this result to immediately get a proof of Craig's interpolation. Lastly, and if time allows, we sketch how to extend our proof to full linear logic.
[Sau25] Alexis Saurin. Interpolation as Cut-Introduction: On the Computational Content of Craig-Lyndon Interpolation. FSCD 2025. https://doi.org/10.4230/LIPIcs.FSCD.2025.32
[FOS25] Guido Fiorillo, Daniel Osorio Valencia, and Alexis Saurin. On Correctness, Sequentialization and Interpolation. TLLA 2025.
[EFP24] Thomas Ehrhard, Claudia Faggian, and Michele Pagani. Bayesian Networks and Proof-Nets: a proof-theoretical account of Bayesian Inference. Technical Report. https://doi.org/10.48550/arXiv.2412.20540

We present an implementation of proof-nets for unit-free multiplicative linear logic in the proof assistant Rocq. It contains a definition of proof-structures and proof-nets, a proof of the sequentialization theorem as well as a definition of cut-elimination.

We revisit sequentialization proofs associated with the Danos-Regnier correctness criterion in the theory of proof nets of linear logic. Our approach relies on a generalization of Yeo's theorem for graphs, based on colorings of half-edges. This happens to be the appropriate level of abstraction to extract sequentiality information from a proof net without modifying its graph structure. We thus obtain different ways of recovering a sequent calculus derivation from a proof net inductively, by relying on a splitting par-vertex, on a splitting tensor-vertex, on a splitting terminal vertex, etc. The proof of our Yeo-style theorem relies on a key lemma that we call cusp minimization. Given a coloring of half-edges, a cusp in a path is a vertex whose adjacent half-edges in the path have the same color. And, given a cycle with at least one cusp and subject to suitable hypotheses, cusp minimization constructs a cycle with strictly less cusps. In the absence of cusp-free cycles, cusp minimization is then enough to ensure the existence of a splitting vertex, i.e. a vertex that is a cusp of any cycle it belongs to. Our theorem subsumes several graph-theoretical results, including some known to be equivalent to Yeo's theorem. The novelty is that they can be derived in a straightforward way, just by defining a dedicated coloring, again without any modification of the underlying graph structure (vertices and edges) - similar results from the literature required more involved encodings.

In a logical system, deciding whether two proofs, or two formulas, are equal is often complicated. Indeed, one usually does not want to identify only proofs that are syntactically equal, i.e. whose rules are exactly the same. In many sequent calculi, there is a cut rule that allows for computation - through a process called cut-elimination - and one wishes for two proofs related by such a computation to be equivalent. Looking at programs through the Curry-Howard correspondence, even if 2 + 2 and (1 + 2) + 1 are not strictly the same term, it is still very sensible to identify them. Another notion of identity on proofs is axiom-expansion, corresponding to the fact that a function f should be considered the same as x ↦ f(x), the function that takes an input x and returns f(x), which is again very natural to ask for. Hence, proofs are seen as equivalent up to these two relations (at least), which in many logical systems is either a trivial nonsense or a combinatorial nightmare. Furthermore, these equalities between proofs yield a notion of equality between formulas, called isomorphism. Two formulas A and B are isomorphic if there are proofs between them whose compositions yield identities - up to the above equivalence relations. Intuitively, this means there is a loseless encoding between A and B, and thus they can be considered as the same; for instance, every use of A can be replaced with one use of B. I will present and give a survey of these two problems of equalities in the framework of linear logic.

In a logical system, deciding whether two proofs (or two formulas) are equal is usually complicated. Indeed, one usually does not want to identify only proofs that are syntactically equal, i.e. whose rules are exactly the same. In many sequent calculi, there is a cut rule that allows for computation - through a process called cut-elimination - and one wishes for two proofs related by such a computation to be the same. Looking at programs through the Curry-Howard correspondence, even if 2 + 2 and (1 + 2) + 1 are not strictly the same term, it is still very sensible to identify them. Another notion of identity on proofs is axiom-expansion, corresponding to the fact that a function f should be considered the same as x ↦ f(x), the function that takes an input x and returns f(x), which is again very natural to ask for. Hence, proofs are seen as equivalent up to these two relations, which in general is either a trivial nonsense or a combinatorial nightmare. Furthermore, these equalities between proofs yield a notion of equality between formulas, called isomorphism. Two formulas A and B are isomorphic if there are proofs between them whose compositions yield identities - up to the above equivalence relations. Intuitively, this means there is a loseless encoding between A and B, and thus they can be considered as the same; for instance, every use of A can be replaced with one use of B. I will present this problem of equalities, in the setting of lambda-calculus and linear logic, along with some known results and difficulties.

We revisit sequentialization proofs associated with the Danos-Regnier correctness criterion in the theory of proof nets of linear logic. Our approach relies on a generalization of Yeo's theorem for graphs, based on colorings of half-edges. This happens to be the appropriate level of abstraction to extract sequentiality information from a proof net without modifying its graph structure. We thus obtain different ways of recovering a sequent calculus derivation from a proof net inductively, by relying on a splitting par-vertex, on a splitting tensor-vertex, on a splitting terminal vertex, etc. The proof of our Yeo-style theorem relies on a key lemma that we call cusp minimization. Given a coloring of half-edges, a cusp in a path is a vertex whose adjacent half-edges in the path have the same color. And, given a cycle with at least one cusp and subject to suitable hypotheses, cusp minimization constructs a cycle with strictly less cusps. In the absence of cusp-free cycles, cusp minimization is then enough to ensure the existence of a splitting vertex, i.e. a vertex that is a cusp of any cycle it belongs to. Our theorem subsumes several graph-theoretical results, including some known to be equivalent to Yeo's theorem. The novelty is that they can be derived in a straightforward way, just by defining a dedicated coloring, again without any modification of the underlying graph structure (vertices and edges); similar results from the literature required more involved encodings.
(Joint work with Olivier Laurent, Lorenzo Tortora de Falco and Lionel Vaux Auclair.)

Les réseaux de preuve sont une contribution majeure de la logique linéaire. Contrairement aux représentations usuelles des preuves comme des arbres de dérivation, un réseau représente une preuve comme un graphe respectant certaines contraintes. Cette syntaxe graphique a de meilleures propriétés, mais n'est pas inductive. Cela explique que malgré une littérature pléthorique sur papier, il y a très peu de formalisations dans des assistants de preuve sur ce sujet : l'obstacle principal est la manipulation de (multi-)graphes sur ordinateur. Je vais présenter une formalisation de ces objets en Rocq/Coq, avec leur définition et quelques résultats standards. En particulier, je vais appuyer sur les difficultés rencontrées et les solutions trouvées en réponse.
(Travail issu majoritairement de ma thèse, supervisée par Olivier Laurent.)

Proof-nets are a major contribution from linear logic. Contrary to the usual representation of proofs as derivation trees in sequent calculus, proof-nets represent proofs as general graphs respecting some correctness criterion. A standard result is that these two syntaxes correspond to each other, which is called sequentialization. Despite being a well-known theorem, its proofs in the literature are generally complex. I will present a new simple proof for proof-nets of multiplicative linear logic, modular enough to still apply in the presence of the mix-rule. Then, I will develop links between sequentialization and more general graph theory, following on works from Rétoré and Nguyen but focusing on edge-colored graphs instead of perfect matchings.
(Joint work with Olivier Laurent, Lorenzo Tortora de Falco and Lionel Vaux Auclair.)

Cet exposé présentera une preuve simple du théorème de Yeo [1], après avoir donné les usuelles notions de théorie des graphes nécessaires (chemin, cycle, coloriage d'arêtes, ...). Cette démonstration est basée sur un nouveau résultat facile à montrer : le saut à l'élastique. Je discuterai ensuite rapidement, si le temps le permet, de généralisations et d'applications de ce théorème.
[1] Anders Yeo. "A Note on Alternating Cycles in Edge-Coloured Graphs". In: Journal of Combinatorial Theory, Series B 69.2 (1997), pp. 222-225.

Given formulas A and B, A is a retraction of B if there exist proofs of A |- B and B |- A which compose to the axiom on A, up to cut-elimination and axiom-expansion. This gives a natural notion of sub-tying, and corresponds to retractions in the category of proofs: objects are formulas, and morphisms proofs up to cut-elimination and axiom-expansion. While isomorphisms for multiplicative linear logic have been characterized (Balat & Di Cosmo gave a corresponding equational theory in 1999), and there is a well-known retraction (which is not an isomorphism), there is not even a conjecture on what the set of retractions could be. I will present a work in progress about this problem, giving properties showing the problem should not be too hard, then solving the case "an atom X is a retraction of a formula B" using proof nets. Meanwhile, I will also show difficulties for solving the general case, as well as what happens in other fragments of linear logic.

Given formulas A and B, A is a retraction of B if there exist proofs of A |- B and B |- A which compose to the axiom on A, up to cut-elimination and axiom-expansion. This gives a natural notion of sub-tying, and corresponds to retractions in the category of proofs: objects are formulas, and morphisms proofs up to cut-elimination and axiom-expansion. While isomorphisms for multiplicative linear logic have been characterized (Balat & Di Cosmo gave a corresponding equational theory in 1999), and there is a well-known retraction (which is not an isomorphism), there is not even a conjecture on what the set of retractions could be. I will present a work in progress about this problem, giving properties showing the problem should not be too hard, then solving the case "an atom X is a retraction of a formula B" using proof nets. Meanwhile, I will also show difficulties for solving the general case, as well as what happens in other fragments of linear logic.

Je vais parler de rétraction en logique. Pour des formules A et B, A est une rétraction de B s'il existe des preuves de A |- B et B |- A dont la composition par coupure sur B est égale à l'axiome sur A, à élimination des coupures et expansion des axiomes près. Cela correspond aux rétractions dans la catégorie des preuves : les objets sont des formules, les morphismes des preuves (considérées à élimination des coupures et expansion des axiomes près), la composition est la coupure et les identités les axiomes. Alors que les isomorphismes de MLL sont connus (Balat et Di Cosmo ont donné une théorie équationnelle correspondante), et qu'il y a une rétraction (qui n'est pas un isomorphisme) de bien connue, il n'y a même pas d'hypothèse sur ce que pourraient être l'ensemble des rétractions. Je vais présenter un travail en cours sur les rétractions de la forme "un atome X est une rétraction de B", et quelles sont les difficultés pour étendre ce résultat au cas de formules quelconques.

We characterize type isomorphisms in the multiplicative-additive fragment of linear logic (MALL), and thus for *-autonomous categories with finite products, extending a result for the multiplicative fragment by Balat and Di Cosmo. This yields a much richer equational theory involving distributivity and annihilation laws. The unit-free case is given by relying on the proof-net syntax introduced by Hughes and Van Glabbeek. We then use the sequent calculus to extend our results to full MALL (including all units).

We propose a new proof of sequentialization for the proof nets of unit-free multiplicative linear logic with mix. It is based on the search of a splitting par by means of a simple new lemma about proof structures: the bungee jumping lemma.

We will present proof nets for unit-free multiplicative linear logic (MLL) before giving a new simple proof of the sequentialization theorem, the key result affirming that proof-nets do indeed represent proofs. This simple proof holds in the presence of the mix rule, and is robust enough to be adapted to proof nets with the additive connectives.

We will speak about isomorphisms in logic. Two formulas A and B are isomorphic if there are proofs of A |- B and of B |- A such that their composition by cut over B (resp. A) is equal to the axiom of A (resp. B) up to cut elimination and axiom expansion. This corresponds to isomorphisms in the category of proofs: objects are formulas, morphisms are proofs (up to cut elimination and axiom expansion), composition is cut and identities are axioms. The problem of characterizing isomorphisms in Multiplicative Linear Logic was already solved by Balat and Di Cosmo. They proved that isomorphisms correspond to associativity and commutativity of the connectives tensor and par, as well as neutrality of the units one and bottom. Their proof uses in an essential way proof nets, an alternative representation of proofs with respect to proof trees. The case of Multiplicative-Additive Linear Logic, with the additive connectives plus and with, is more complex because of the distributive laws of the tensor over the plus and of the par over the with. During this presentation, we will introduce the notion of isomorphism in different settings, before giving an overview of the proof from Balat and Di Cosmo and then explaining how to extend it in the presence of additives.

We propose a new proof of sequentialization for the proof nets of unit-free multiplicative-additive linear logic of Hughes & Van Glabbeek. This is done by adapting a method from unit-free multiplicative linear logic, showing the robustness of this approach.