BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Typed realizability for first-order classical analysis - Valentin 
 Blot\,  Mathematical foundations group\, computer science department\, Uni
 versity of Bath
DTSTART:20151127T140000Z
DTEND:20151127T150000Z
UID:TALK62501@talks.cam.ac.uk
CONTACT:Ohad Kammar
DESCRIPTION:We describe a realizability framework for classical first-orde
 r logic\nin which realizers live in (a model of) typed lambda-mu-calculus.
  This\nallows a direct interpretation of classical proofs\, avoiding the u
 sual\nnegative translation to intuitionistic logic. We prove that the usua
 l\nterms of Gödel's system T realize the axioms of Peano arithmetic\, and
 \nthat under some assumptions on the computational model\, the bar\nrecurs
 ion operator realizes the axiom of dependent choice. We also\nperform a pr
 oper analysis of relativization\, which allows for less\ntechnical proofs 
 of adequacy. Extraction of algorithms from proofs of\npi-0-2 formulas reli
 es on a novel implementation of Friedman's trick\nexploiting the control p
 ossibilities of the language. This allows to\nhave extracted programs with
  simpler types than in the case of negative\ntranslation followed by intui
 tionistic realizability.
\n
LOCATION:FW26
END:VEVENT
END:VCALENDAR