Séminaire, Oct. 17, 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)
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 biorthogonalitybased realizability. As we will see, by considering different FCAs, we obtain realizability frameworks for various programming languages (for example featuring higherorder references, recursive types, boundedtime/space execution, streams, etc.), all sharing a common soundness result.
I will also show how the wellknown 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 (realvalued) 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 "UpperExpectation bisimilarity" using standard results of linear algebra and functional analysis and provide strong mathematical foundations for realvalued modal logics for PNTS's.