Realizability games for the specification problem

Carte non disponible

Date/heure
Date(s) - 02/07/2015
11 h 00 min - 12 h 00 min

Catégories


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/]

Olivier CHABROL
Posts created 14

Articles similaires

Commencez à saisir votre recherche ci-dessus et pressez Entrée pour rechercher. ESC pour annuler.

Retour en haut
Secured By miniOrange