Séminaire, Oct. 17, 2013


La rencontre aura lieu à l'École Normale Supérieure de Lyon, campus Jacques Monod, dans l'amphi B. Pour venir, voir les instructions sur le site du LIP ou sur un plan, par exemple chez Google Maps. À l'entrée, se présenter à la réception, qui aura la liste des inscrits.


10:30 – 12:00
Guillaume Brunerie (Univ. Nice Sophia Antipolis)

I will give an overview of homotopy type theory (HoTT), a field combining abstract homotopy theory with dependent type theory. I will then explain the problem of computing homotopy groups of spheres and how it relates to homotopy type theory.

14:00 – 15:00
Aloïs Brunel (Univ. Paris 13)

In this talk, I will present the monitoring calculus, which is the result of a new forcing program transformation. It's a lambda calculus with a state that is able to monitor the execution of programs (this "monitoring" being a parameter of the machine). This mechanism is similar to what happens in Miquel's KFAM (Krivine Forcing Abstract Machine).

Based on this calculus, I define the notion of Forcing Computational Algebra (FCA), which internalizes the composition of linear forcing with a more usual biorthogonality-based realizability. As we will see, by considering different FCAs, we obtain realizability frameworks for various programming languages (for example featuring higher-order references, recursive types, bounded-time/space execution, streams, etc.), all sharing a common soundness result.

I will also show how the well-known technique of iterated forcing corresponds in our framework to a certain construction on FCAs, allowing us to combine different programming features in a modular way.

The ultimate goal of this work is to obtain a general, modular, algebraic framework in which we design and combine realizability models for all kind of programming languages.

15:30 – 16:30
Matteo Mio (CWI, Amsterdam)

Several notions of bisimulation for Probabilistic Nondeterministic Transition Systems (PNTS) have been proposed in the literature. We develop the theory of what we call "Upper-Expectation bisimilarity" using standard results of linear algebra and functional analysis and provide strong mathematical foundations for real-valued modal logics for PNTS's.