Réunion ANR Récré, April 11, 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

Nicolas Tabareau (INRIA, Inventeurs du monde numérique)Invited talk: Univalence for free, not yet ...
We present an internalization of the 2groupoid (or rather groupoidoid) interpretation of the calculus of construction that allows to realize proof irrelevance, reasoning modulo and a weak form of the univalence axiom. As an example, we show that in our setting, the type of Church integers is equal to the inductive type of natural numbers.
 14:00 – 15:00

Colin Riba (ENS Lyon)Invited talk: Forcing MSO on Infinite Words in Weak MSO
We propose a forcingbased interpretation of monadic secondorder logic (MSO) on !words in Weak MSO (WMSO). The interpretation is purely syntactic and compositional. We show that a formula with parameters is true in MSO if and only if its interpretation is true in WMSO. We also show that a closed formula is true in MSO if and only if its interpretation is provable under some axioms which hold for WMSO, but without axiomatizing it. We use modeltheoretic arguments. Our approach is inspired from pointfree topology: infinite words, seen as topological points, are approximated by filters of bounded segments. We devise forcing conditions such that the corresponding generic filters approximate Ramseyan factorizations of infinite words modulo satisfaction of formulas of a given quantifier depth. Our interpretation parallels some approaches to Mc Naughton?s Theorem (equivalence between nondeterministic B¨uchi automata and deterministic Rabin automata) but the obtained formulas do not by themselves describe deterministic automata.
 15:30 – 16:30

Guillaume MunchMaccagnoni (Univ. Paris 7)Invited talk: When composition is not associative
Strict and lazy composition (in the presence of evaluation order) do not associate. The phenomenon was observed multiple times in semantics (programming, proof theory).
Nonassociativity is not only ubiquitous but also characterises by itself notions of computation with nontrivial evaluation order, as we will see.