BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:On normalization for the typed λ-calculus - Simon Castellan
DTSTART:20161111T104500Z
DTEND:20161111T114500Z
UID:TALK69143@talks.cam.ac.uk
CONTACT:Ian Orton
DESCRIPTION:In this talk\, I will investigate normalization proof for seve
 ral typed\nλ-calculi on their relationship with logic.\n\nI will start wi
 th the simply-typed λ-calculus and the "classic"\ntermination proof using
  realizability. I will discuss the computational\nmeaning of this proof in
  terms of normalization by evaluation (Following\nrecent work by Gabriel S
 cherer) and mention the expressivity of the\nsimply-typed λ-calculus in t
 erms of ordinal complexity.\n\nI will then move on to Gödel's system T\, 
 extend the proof and present\nthe connection with 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 Ge
 ntzen's one using\ntransfinite induction. Finally\, I move to Girard's sys
 tem F and the link\nwith PA2.\n\nI will assume basic familarity with the c
 alculus in question\n(simply-typed\, T\, F) and the logics associated (Pro
 positional logical\,\nPA1\, PA2).
LOCATION:Rainbow Room (FS07)\, Computer Laboratory
END:VEVENT
END:VCALENDAR