Abstract

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.