Rencontre, 8 février 2018

Programme

10:30 – 12:00

Prakash Panangaden (Mc Gill University, Canada)

Invited talk: Quantitative Equational Logic

Equational reasoning is a central part of mathematics. The traditional theory links the equational logic and monads on the category of sets. More precisely, one can define an algebraic theory by giving a set of operations and equations. One can then show that the collection of algebras defined by these equations form the algebras for a monad on the category of sets. One has classical theorems like the completeness and variety theorems of Birkhoff. We consider a modified notion of equation where the equality symbol is annotated with a real number so we can write s =_e t with the interpretation that the terms "s" and "t" are within "e" of each other. We develop the metatheory and obtain analogues of Birkhoff's theorem. Furthermore, we show that this extended notion of equational definition yields algebras of monads on the category of metric spaces. What makes the theory interesting is the fact that well known metric spaces of probability distributions can be defined by such equations.

This is joint work with Radu Mardare and Gordon Plotkin.

14:00 – 15:00

Justin Hsu (University College London, UK)

Invited talk: From Couplings to Probabilistic Relational Program Logics

Many program properties are relational, comparing the behavior of a program (or even two different programs) on two different inputs. While researchers have developed various techniques for verifying such properties for standard, deterministic programs, relational properties for probabilistic programs have been more challenging. In this talk, I will survey recent developments targeting a range of probabilistic relational properties, with motivations from privacy, cryptography, machine learning. The key idea is to meld relational program logics with an idea from probability theory, called a probabilistic coupling. The logics allow a highly compositional and surprisingly general style of analysis, supporting clean proofs for a variety of probabilistic relational properties.

15:30 – 16:30

Thomas Ehrhard (IRIF, Univ. Paris Diderot)

Invited talk: Stable and measurable functions on positive cones: a model of probabilistic functional languages with continuous types

Joint work with Michele Pagani and Christine Tasson

The Probabilistic Coherence Space (PCS) model provides a denotational semantics for probabilistic functional languages (with full recursion and recursive types) where programs are interpreted as power series with non-negative real coefficients. It has interesting properties (such as a Full Abstraction property), but seems to be essentially limited to discrete probabilities. To overcome this limitation, we replace PCSs with positive cones, which generalize them quite naturally, and power series with Scott-continuous functions which are "stable" in a sense that we will explain. A typical object of this new model is the cone of finite measures on the real line which seems impossible to represent as a PCS. Raphaëlle Crubillé has shown recently that this extension of the PCS model is conservative.