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 &\; Semantics for Dummies
SUMMARY:On normalization for the typed λ-calculus - Simon
Castellan
DTSTART;TZID=Europe/London:20161111T104500
DTEND;TZID=Europe/London:20161111T114500
UID:TALK69143AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/69143
DESCRIPTION:In this talk\, I will investigate normalization pr
oof for several typed\nλ-calculi on their relation
ship with logic.\n\nI will start with the simply-t
yped λ-calculus and the "classic"\ntermination pro
of using realizability. I will discuss the computa
tional\nmeaning of this proof in terms of normaliz
ation by evaluation (Following\nrecent work by Gab
riel Scherer) and mention the expressivity of the\
nsimply-typed λ-calculus in terms of ordinal compl
exity.\n\nI will then move on to Gödel's system T\
, extend the proof and present\nthe connection wit
h PA1\, Peano's arithmetic and how to deduce from\
nstrong normalization of T\, consistency of PA_1.
I will (try to) comment\non the link between this
consistency proof and Gentzen's one using\ntransfi
nite induction. Finally\, I move to Girard's syste
m F and the link\nwith PA2.\n\nI will assume basic
familarity with the calculus in question\n(simply
-typed\, T\, F) and the logics associated (Proposi
tional logical\,\nPA1\, PA2).
LOCATION:Rainbow Room (FS07)\, Computer Laboratory
CONTACT:Ian Orton
END:VEVENT
END:VCALENDAR