University of Cambridge > Talks.cam > Churchill CompSci Talks > Curry-Howard Correspondence: Dependent Types and First Order Intuitionistic Logic

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

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity