Inauguration Récré, 12 janvier 2012
Journée inaugurale du projet ANR Récré.
Lieu
La journée aura lieu à l'École Normale Supérieure de Lyon, campus Jacques Monod, dans l'amphi E. 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:00 – 10:30
-
Olivier Coucharière (Chargé de mission à l'ANR)
- 10:45 – 12:15
-
Thomas Streicher (TU Darmstadt)
The aim of our presentation is to give an account of Krivine's Classical Realizability based on the general categorical approach to realizability developed by Hyland, van Oosten, Hofstra et.al.
We define a notion of abstract Krivine structure (aks) and show how it gives rise to an order pca with a filter. The latter induces a tripos (a categorical model of higher order logic) which in turn gives rise to a Classical Realizability Topos.
We formulate a precise theorem explaining why ordinary forcing is the commutative case of classical realizability.
If time allows it we shall also give an account of forcing within classical realizability considered by Krivine as part of his long term project of realizing full ZFC.
- 14:00 – 15:00
-
Guilhem Jaber (École des Mines de Nantes)
In this talk, I will present an extension of the Calculus of Constructions (the theory behind Coq) which allows to extend modularly the type system with new constructors and new inference rules. The idea is to define a translation between the new system and the original one, following the idea of Krivine and Miquel to study the translation of proofs induced by forcing. Our translation of forcing is is in fact an internalization in the type theory of the topos of presheaves of Birkedal et al.
I will then show how we can use this technique to extend the inductive types of Coq with negative occurrences. This will be used to formalize recent works on Kripke Logical Relations.
- 15:30 – 16:30
-
Hugo Herbelin (PPS/PiR2 - Université Paris Diderot)
From a programming point of view, control operators are effectful operators whose effects can be cleared by using delimiters at base types. From the point of view of logic, it has been shown that by delimiting control operators, i.e. classical logic, on purely positive formulas (an equivalent in predicate logic of Sigma\^0_1-formulas in arithmetic), we obtain a logic that remains essentially intuitionistic (in the sense of satisfying the disjunction and existence properties) but whose logical strength now constructively captures "axioms" such as Markov's principle or the double negation shift.
There is no reason to restrict the delimitation to only control operators and indeed, other kinds of delimited effects such as memory assigments can be considered too. This connects to Cohen's forcing what eventually yields an intuitionistic logic able to prove those axioms that are provably consistent by forcing.
