|
2 videos available for this event!
|
Logic of Probabilistic Programming
Logique de la programmation probabiliste
31 January – 4 February 2022
|
Scientific Committee
Comité scientifique Ugo Dal Lago (University of Bologna) |
Organizing Committee
Comité d’organisation Martin Avanzini (INIRIA Sophia Antipolis Méditerranée) |
|
Probabilities play an increasing role in computer science. Important deterministically-intractable problems admit feasible approximate probabilistic solutions. Probabilistic algorithms are essential in distributed computing and numerical computing (Monte Carlo methods), not to mention the role of probabilistic methods in deep learning (stochastic gradient). Linear logic shows quite useful in this setting because some of the most basic notions of probability theory are linear: Markov chains or kernels, Bayesian networks etc.
The general purpose of this week is not only to present the state of the art on the applications of proof theory, category theory and denotational semantics to the analysis of probabilistic programs and to the foundation of probabilistic formal methods for program and system verification, but also to stress the specificities of Bayesian programming and machine learning where programs represent statistical models. The program of the week is designed for conveying to the non-specialist a coherent picture of this exciting and very active area. |
Les probabilités jouent un rôle croissant en informatique. Ainsi, des problèmes très importants n’acceptent pas de solution déterministe ou seulement des solutions d’une trop grande complexité, mais deviennent approximativement faisables dans un cadre probabiliste. Les algorithmes probabilistes sont aussi essentiels dans les systèmes distribués, en calcul numérique (méthode de Monte Carlo) etc. Sans parler du rôle essentiel des méthodes probabilistes en deep learning (gradient stochastique). La logique linéaire est ici cruciale car certaines des notions les plus fondamentales de la théorie des probabilités sont de nature essentiellement linéaire : c’est le cas par exemple des chaînes et des noyaux de Markov et des réseaux bayésiens. L’objectif général de cette semaine est non seulement de présenter l’état de l’art sur les applications de la théorie de la démonstration, de la théorie des catégories et de la sémantique dénotationnelle à l’analyse des programmes probabilistes, dans la perspective de la mise au point de méthodes formelles pour la vérification et la validation des programmes et des systèmes, mais aussi de mettre l’accent sur les spécificités de la programmation bayésienne et du machine learning dans laquelle les programmes représentent des modèles statistiques. Le programme de la semaine est conçu de façon à permettre aux chercheurs non spécialistes ou débutants de se faire une idée aussi cohérente que possible de ce sujet en pleine ébullition.
|
Semantics of probabilistic programs (operational and denotational)
Bayesian programming
Differentiable programming
Quantitative tools for probabilistic systems: probabilistic automata, bisimulation, distances, etc.
Randomised computation and cryptography
Verification of probabilistic programs.
Tutorial speakers
Semantics and probabilistic programming :
Raphaëlle Crubillé (CNRS, Marseille) Semantics of probabilistic programming
Ohad Kammar (University of Edimburgh) An introduction to statistical modelling semantics with higher-order measure theory
Bayesian programming languages :
Brooks Paige (University College London) Bayesian Inference in Probabilistic Programs
Matthijs Vákár (Utrecht University) Mathematical foundations of automatic differentiation
Verification of probabilistic systems :
Marta Kwiatkowska (University of Oxford) Probabilistic model checking for strategic equilibria-based decision making
Speakers
Melissa Antonelli (University of Bologna) Towards a Probabilistic Curry-Howard Correspondence
Kevin Batz (RWTH Aachen University) Latticed k-Induction with an Application to Probabilistic Programs
Ulrik Buchholtz (TU Darmstadt) Toposes for probabilistic programming
Thomas Ehrhard (CNRS, Université de Paris) Coherent differentiation
Claudia Faggian (CNRS, Université de Paris) Bayesian Networks and Proof-Nets: a proof-theoretical account of Bayesian Inference
Cameron Freer (MIT) Computability of representations of exchangeable data in probabilistic programming
Marco Gaboardi (Boston University) A Separation Logic for Negative Dependence
Tomáš Gonda (Perimeter Institute for Theoretical Physics of Waterloo) De Finetti’s Theorem in Categorical Probability
Jane Hillston (University of Edinburgh)
Joost-Pieter Katoen (Aachen University) Extending Probabilistic Weakest Preconditions
Lutz Klinkenberg (RWTH Aachen University) Generating Functions for Probabilistic Programs
Annabelle Mc Iver (Macquarie University) Probabilistic Programming for proving privacy
Michele Pagani (Université de Paris) Automatic differentiation in PCF using linear logic negation
Catuscia Palamidessi (INRIA Saclay & LIX) On the impossibility of non-trivial accuracy under fairness constraints
Prakash Panangaden (McGill University) Equivalences for Feller-Dynkin processes –
Philipp Schroer (RWTH Aachen University) Building a deductive verifier for probabilistic programs
Alexandra Silva (Cornwell University) Probabilistic NetKAT
David Tolpin (Ben-Gurion University of the Negev) Probabilistic programs with stochastic conditioning
Dominik Wagner (University of Oxford) A Language and Smoothed Semantics for Convergent Stochastic Gradient Descent
Tobias Winkler (RWTH Aachen University) Model Checking Temporal Properties of Recursive Probabilistic Programs
Fabian Zaiser (University of Oxford) Rigorous bounds for posterior inference in universal probabilistic programming
Vladimir Zamdzhiev (INRIA) Commutative Monads for Probabilistic Programming Languages
Robert Zinkov (University of Oxford) A probabilistic relational language
 |
 |