Rencontre, June 6, 2019


10:30 – 12:00
Ohad Kammar (University of Edinburgh)

We have used Quasi-Borel spaces, a new mathematical structure, as a foundations of probabilistic programming and higher-order statistics. In this talk, I will introduce this alternative to traditional measure theory. We will cover the basic definition, and the constructions relevant to modelling and verification.

14:00 – 15:00
Jérémy Ledent (LIX, École Polytechnique)

Geometric methods have been used for 20 years to prove impossibility results for fault-tolerant concurrent computing. We study these methods from a semantical perspective: in what sense do they constitute a semantics for concurrent programs?

In this talk, I will explain how to derive these geometric models from a concrete operational semantics based on interleavings of execution traces. To do so, I will review and compare different trace-based methods for specifying behaviors of concurrent objects.

15:30 – 16:30
Lutz Strassburger (INRIA Saclay and LIX, École Polytechnique)

In this talk I will give an introduction to combinatorial proofs, explain the motivation behind, and discuss what it means for a proof to be "without syntax". The main emphasis will be on combinatorial proofs for classical and intuitionistic propositional logic.