COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

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 LogicAdd 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:Note that ex-directory lists are not shown. |
## Other listsTEDxOxbridge Centre for Scientific Computing Cambridge Statistics Clinic Aitken Lectures Physics of Medicine (PoM) Seminar Series Cambridge University European Society## Other talksMulti-scale observations of ocean circulation in the Atlantic Holonomic D-modules, b-functions, and coadmissibility Interrogating T cell signalling and effector function in hypoxic environments Stopping the Biological Clock – The Lazarus factor and Pulling Life back from the Edge. Acceleration of tropical cyclogenesis by self-aggregation feedbacks |