Curry-Howard Correspondence: Dependent Types and First Order Intuitionistic Logic

Add to your list(s) Download to your calendar using vCal

• Raahil Shah, Churchill College
• Wednesday 15 October 2014, 19:40-20:30
• Wolfson Hall, Churchill College.

If you have a question about this talk, please contact Jasper Lee.

The Curry-Howard Correspondence relates two seemingly unrelated formalisms – namely logic and computation in the sense of Church’s lambda calculus. The key observation is that some type systems have identical structure with deduction systems for some logics. As a result, types encode logical statements, and programs of such types are proofs of such 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 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 comments on the implications of the correspondence on non-terminating programs and the decidability of logic.

This talk is part of the Churchill CompSci Talks series.

This talk is included in these lists:

• Churchill CompSci Talks
• Wolfson Hall, Churchill College
• computer science
• se393's list

Note that ex-directory lists are not shown.