Realizability games for the specification problem
Etienne Miquey
PPS, Université Paris-Diderot
http://perso.ens-lyon.fr/etienne.miquey/
Date(s) : 02/07/2015 iCal
11h00 - 12h00
In Krivine classical realizability, one can understand the truth value of a formula (that is the set of its realizers) as its defenders, and the falsity value as the set of its opponents. Following this intuition, the execution of a process is a match between both players, that a realizer should win.
–
In this talk, we will explain how to use a notion of game to give a precise specification of the realizers of a given formula. We will focus on the particular case of arithmetical formulae, for which our definition relies on the principle of Coquand’s games. In the end, we obtain an equivalence between universal realizers and winning strategies (even in presence of non-substitutive instructions such as Quote), which also directly implies the absoluteness of arithmetical formulae for classical realizability.
–
http://www.pps.univ-paris-diderot.fr/~emiquey/
Catégories
