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:7946@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20151210T140000
DTEND;TZID=Europe/Paris:20151210T150000
DTSTAMP:20241120T205611Z
URL:https://www.i2m.univ-amu.fr/evenements/typed-realizability-for-first-o
 rder-classical-analysis/
SUMMARY:Valentin Blot (University of Bath): Typed realizability for first-o
 rder classical analysis
DESCRIPTION:Valentin Blot: We describe a realizability framework for classi
 cal first-order logic in which realizers live in (a model of) typed lambda
 -mu-calculus. This allows a direct interpretation of classical proofs\, av
 oiding the usual negative translation to intuitionistic logic. We prove th
 at (the interpretations of) the usual terms of Gödel's system T realize t
 he axioms of Peano arithmetic\, and that under some assumptions on the com
 putational model\, the bar recursion operator realizes the axiom of depend
 ent choice. We also perform a proper analysis of relativization\, which al
 lows for less technical proofs of adequacy. Extraction of algorithms from 
 proofs of pi-0-2 formulas relies on a novel implementation of Friedman's t
 rick exploiting the control possibilities of the language. This allows to 
 have extracted programs with simpler types than in the case of negative tr
 anslation followed by intuitionistic realizability.\n\n
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Valentin_Blot.jpg
CATEGORIES:Séminaire,Logique et Interactions
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20151025T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR