Séminaire, 17 octobre 2013

Lieu

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.

Programme

10:30 – 12:00
Guillaume Brunerie (Univ. Nice Sophia Antipolis)
Invited talk: Homotopy type theory and homotopy groups of spheres

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)
Invited talk: Composing forcing and classical realizability: the monitoring calculus

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)
Invited talk: Semantic Foundations of Quantitative (real-valued) Logics based on Functional Analysis

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.