BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:Typed realizability for first-order classical anal
 ysis - Valentin Blot\,  Mathematical foundations g
 roup\, computer science department\, University of
  Bath
DTSTART;TZID=Europe/London:20151127T140000
DTEND;TZID=Europe/London:20151127T150000
UID:TALK62501AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/62501
DESCRIPTION:We describe a realizability framework for classica
 l first-order logic\nin which realizers live in (a
  model of) typed lambda-mu-calculus. This\nallows 
 a direct interpretation of classical proofs\, avoi
 ding the usual\nnegative translation to intuitioni
 stic logic. We prove that the usual\nterms of Göde
 l's system T realize the axioms of Peano arithmeti
 c\, and\nthat under some assumptions on the comput
 ational model\, the bar\nrecursion operator realiz
 es the axiom of dependent choice. We also\nperform
  a proper analysis of relativization\, which allow
 s for less\ntechnical proofs of adequacy. Extracti
 on of algorithms from proofs of\npi-0-2 formulas r
 elies on a novel implementation of Friedman's tric
 k\nexploiting the control possibilities of the lan
 guage. This allows to\nhave extracted programs wit
 h simpler types than in the case of negative\ntran
 slation followed by intuitionistic realizability.

 \n
LOCATION:FW26
CONTACT:Ohad Kammar
END:VEVENT
END:VCALENDAR