BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Curry-Howard Correspondence: Dependent Types and First Order Intui
 tionistic Logic - Raahil Shah\, Churchill College
DTSTART:20141015T184000Z
DTEND:20141015T193000Z
UID:TALK55490@talks.cam.ac.uk
CONTACT:Jasper Lee
DESCRIPTION:The Curry-Howard Correspondence relates two seemingly unrelate
 d formalisms - namely logic and computation in the sense of Church’s lam
 bda calculus. The key observation is that some type systems have identical
  structure with deduction systems for some logics. As a result\, types enc
 ode logical statements\, and programs of such types are proofs of such sta
 tements. This talk will first introduce the Curry-Howard Correspondence on
  the simple example of simply typed lambda calculus and propositional intu
 itionistic logic. I will then describe the dependent product and dependent
  sum types and demonstrate their use. Following that will be a description
  of first order intuitionistic logic. Remarkably\, this logic corresponds 
 to dependent types\, which I will explain. I will conclude the talk with c
 omments on the implications of the correspondence on non-terminating progr
 ams and the decidability of logic.
LOCATION:Wolfson Hall\, Churchill College
END:VEVENT
END:VCALENDAR