BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//wp-events-plugin.com//7.2.3.1//EN
TZID:Europe/Paris
X-WR-TIMEZONE:Europe/Paris
BEGIN:VEVENT
UID:8123@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20150326T110000
DTEND;TZID=Europe/Paris:20150326T123000
DTSTAMP:20241120T210036Z
URL:https://www.i2m.univ-amu.fr/evenements/bar-recursion-semantique-denota
 tionnelle-et-realisabilite-classique/
SUMMARY:Jean-Louis Krivine (PPS\, Université Paris-Diderot): Bar recursion
 \, sémantique dénotationnelle et réalisabilité classique
DESCRIPTION:Jean-Louis Krivine: L'opérateur de bar recursion\, introduit d
 ans les années 60 par C. Spector pour "prouver" la consistance de l'Analy
 se\, 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).\nUne autre méthode pour ce faire est\
 , en réalisabilité classique\, d'utiliser une instruction "quote". La qu
 estion 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 d
 e sémantique dénotationnelle\, où "quote" n'a aucun sens. On verra auss
 i que\, dans ces modèles\, cet opérateur fournit des programmes pour l'a
 xiome du bon ordre sur R\, et pour toutes les formules "vraies" d'Analyse.
 \n\nhttp://www.pps.univ-paris-diderot.fr/~krivine/
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Jean-Louis_Krivine.jpg
CATEGORIES:Séminaire,Logique et Interactions
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20141026T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR