After successful completion of the course, students are able to learn new methods in Type Theory and Proof Theory and to apply them independently. In particular the students are able to establish connections between Computational Logic and Functional Programming.
Intuitionistic Logic, simply typed Lambda-Calculus, Curry-Howard Isomorphism, first-order arithmetic, system T, second-order logic, system F.
Preparation of chapters by the students, working out a presentation together with the lecturer. Discussions of the topics in the group.
The seminar is based on Sørensen, Urzyczyn: "Lectures on the Curry-Howard Isomorphism" (2006) which can be accessed via https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/149/suppl/C using the university network.
Grading in this course is based on a talk to be given in the seminar and on participation.
Not necessary
Firm knowledge in Mathematical Logic.
