The aim is to master techniques of Lambda-calculus and computational proof theory
typed Lambda-calculus. The systems T and F, intuitionistic logic, Curry-Howard isomorphism, Peano arithmetic and Heyting arithmetic, consistency of Peano arithmetic and of Heyting arithmetic
beginning of the course on October 10, 2017, 15:00, Seminar Room Goedel, Favoritenstrasse 9, ground floor.
For completing the course the student has to give two talks on the material.
Not necessary
Solid background in logic, basic knowledge in Lambda-Calculus
