Learn how to use and reason about lambda calculus and types. Learn the fundamental notions of the famous connection between logical proofs and typed lambda terms.
We introduce the lambda calculus, the mathematical base of functional programming language. We then show how to map lambda terms into types, that is, logical formulas describing computational properties of programs. This connection between logic and lambda calculus is known as Curry-Howard correspondence.
The course will start on March 11th. The classes will be every Monday 17:00-19:00
Written exam
Firm knowledge of classical propositional and first-order logic
