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:Churchill CompSci Talks
SUMMARY:Curry-Howard Correspondence: Dependent Types and F
irst Order Intuitionistic Logic - Raahil Shah\, Ch
urchill College
DTSTART;TZID=Europe/London:20141015T194000
DTEND;TZID=Europe/London:20141015T203000
UID:TALK55490AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/55490
DESCRIPTION:The Curry-Howard Correspondence relates two seemin
gly unrelated formalisms - namely logic and comput
ation in the sense of Churchâ€™s lambda calculus. Th
e key observation is that some type systems have i
dentical structure with deduction systems for some
logics. As a result\, types encode logical statem
ents\, and programs of such types are proofs of su
ch statements. This talk will first introduce the
Curry-Howard Correspondence on the simple example
of simply typed lambda calculus and propositional
intuitionistic logic. I will then describe the dep
endent product and dependent sum types and demonst
rate their use. Following that will be a descripti
on of first order intuitionistic logic. Remarkably
\, this logic corresponds to dependent types\, whi
ch I will explain. I will conclude the talk with c
omments on the implications of the correspondence
on non-terminating programs and the decidability o
f logic.
LOCATION:Wolfson Hall\, Churchill College
CONTACT:Jasper Lee
END:VEVENT
END:VCALENDAR