Rencontre, 6 juin 2019

Programme

10:30 – 12:00

Ohad Kammar (University of Edinburgh)

Invited talk: A tutorial on quasi-Borel spaces

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)

Invited talk: Geometric semantics for asynchronous computability

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.

• slides

15:30 – 16:30

Lutz Strassburger (INRIA Saclay and LIX, École Polytechnique)

Invited talk: Introduction to Combinatorial Proofs

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.