Séminaire, 11 décembre 2025

Programme

10:30 – 11:45

Hugo Paquet (Antique, INRIA)

Invited talk: Monads and algebras for efficient inference in probabilistic programming

Computing the output distribution of a discrete probabilistic program (a process known as exact inference) can be very slow if implemented naively. A common solution is to use efficient representations of probability distributions as trees of random variables.

We have developed a new semantic model for probabilistic programming that captures this kind of optimization. The model is compositional, making it easy to explain why the optimization is correct with respect to the standard semantics of probabilistic programming.

In this talk, I will explain the construction in detail. The key idea is to decompose the probabilistic effect into two effects: name generation (for creating new random variables) and read-only state (for branching on sampled values). The main technical challenge is to correctly combine the monadic semantics of call-by-value for the first effect with call-by-name for the second.

This is based on a joint work with Aurore Alcolei, Simon Castellan, and Tom Hirschowitz.

13:45 – 14:45

Kostia Chardonnet (Mocqua, INRIA)

Invited talk: Compiling Quantum λ-Terms into Circuits via the Geometry of Interaction

We present an algorithm turning any term of a linear quantum λ-calculus into a quantum circuit. The essential ingredient behind the proposed algorithm is Girard's geometry of interaction, which, differently from its well-known uses from the literature, is here leveraged to perform as much of the classical computation as possible, while producing a circuit that, when executed, performs all the quantum operations in the underlying λ-term. Noticeably, we identify a class of terms which can be compiled without an exponential blowup, which is encountered when using plain operational semantics.

15:15 – 16:15

Julie Cailler (LORIA, Nancy)

Invited talk: Deskolemization: From Tableaux to Machine-Checkable Proofs

Bridging the gap between automated and interactive theorem provers remains one of the major challenges in formal reasoning. Automated theorem provers can generate proofs very efficiently, but their internal proof representations are usually not readily translatable into proofs checkable by interactive theorem provers. Techniques such as the analytic tableau method are, in principle, well suited to produce proofs that can be certified, but things get more complicated when we use more advanced proof-search strategies — e.g., Skolemization — that transform the structure of the proof.

In this talk, we will discuss how this problem can be addressed through deskolemization, the process of reconstructing the logical structure of tableau proofs that rely on different Skolemization strategies. We will present a generic deskolemization framework, implemented in the Goéland prover, and show how the resulting proofs can be exported and verified in systems such as Rocq, Lambdapi, SC-TPTP and Lisa.