The talks are organised as the activities of the project Linear Logic And Probabilistic Programming LILOPRO, which is a bilateral project between Serbia and France within the program Pavle Savić - Hubert Curien Partnership.
date/vreme: sreda, 01/07/2026, 12:00
venue/mesto: sala za sastanke na 3. spratu u KULI FTN
Speaker/Predavač:
Prof. Michele Pagani, École Normale Supérieure de Lyon, https://perso.ens-lyon.fr/michele.pagani/
Title/Naslov: Variable Elimination as Rewriting in a Linear Lambda Calculus
Abstract/Sažetak: Variable Elimination (VE) is a classical exact inference algorithm for probabilistic graphical models such as Bayesian Networks, computing the marginal distribution of a subset of the random variables in the model. Our goal is to understand Variable Elimination as an algorithm acting on programs in an idealized probabilistic functional language—a linear simply-typed λ-calculus suffices for our purpose. Precisely, we express VE as a term rewriting process, which transforms a global definition of a variable into a local definition, by swapping and nesting let-in expressions. We exploit in an essential way linear types. (Joint work with Claudia Faggian and Thomas Ehrhard)
Speaker/Predavač:
Dr. Matteo Mio, École Normale Supérieure de Lyon, https://perso.ens-lyon.fr/matteo.mio/
Title/Naslov: Compact Quantitative Equational Theories as Monad Restrictions
Abstract/Sažetak: Proofs in quantitative algebra are, generally, infinite objects due to the presence of infinitary rules in the deductive apparatus. A quantitative equational theory is called compact if all its consequences are derivable by means of finite proofs, that is, proofs not using any instances of the infinitary rules. This definition is purely logical. In this work we give an equivalent, but categorical, characterization based on the notion of monad restriction. (Joint work with Colin Riba from ENS de Lyon)
Speaker/Predavač:
Junior Prof. Paolo Pistone, École Normale Supérieure de Lyon, https://perso.ens-lyon.fr/paolo.pistone/
Title/Naslov: The garden of forking paths: an excursion between probabilistic programming, logic and combinatorics
Abstract/Sažetak: In probabilistic programming users can delegate choices to be made during computation to external random events, like the rolling of a dice. In some situations, this leads to finding, quickly and with high probability, solutions that it would otherwise be very hard to find by a purely deterministic approach. At the same time, the analysis of probabilistic programs is often difficult, since one has to consider all possible computational trajectories, giving rise to complex combinatorial spaces. In particular, from a logical point of view, while properties of deterministic programs like termination are notoriously undecidable, verifying the corresponding properties of probabilistic programs is often an even "more undecidable" problem (i.e. placed strictly higher in the arithmetical hierarchy). In this presentation we use ideas coming from combinatorics and linear logic to investigate the intrinsic complexity of verifying termination properties of probabilistic programs. We focus on three problems: determining if a program terminates with probability 1, if its expected running time is finite, and predicting its most likely execution paths. Notably, by relying on well-known classifications of generating functions in combinatorics, we introduce corresponding classifications of programs with respect to the (un)decidability of these three problems.