Bar recursion, sémantique dénotationnelle et réalisabilité classique

Carte non disponible
Speaker Home page :
Speaker :
Speaker Affiliation :

()

Date/heure
Date(s) - 26/03/2015
11 h 00 min - 12 h 30 min

Catégories


L’opérateur de bar recursion, introduit dans les années 60 par C. Spector pour « prouver » la consistance de l’Analyse, a été recyclé à partir de 1998, par Berardi, Bezem, Coquand, Berger, Oliva, Kohlenbach, … pour obtenir des programmes à l’aide de l’axiome du choix dépendant (DC).
Une autre méthode pour ce faire est, en réalisabilité classique, d’utiliser une instruction « quote ». La question se posait, du rapport entre ces deux méthodes. En fait, on verra que l’opérateur de « bar recursion » ne fonctionne que dans les modèles de sémantique dénotationnelle, où « quote » n’a aucun sens. On verra aussi que, dans ces modèles, cet opérateur fournit des programmes pour l’axiome du bon ordre sur R, et pour toutes les formules « vraies » d’Analyse.

[http://www.pps.univ-paris-diderot.fr/~krivine/]


Retour en haut 

Secured By miniOrange