Lambda Calculus

What it is about

You learn the fundamentals of the lambda calculus as a model of programming languages. First you treat untyped lambda calculus, its reduction rules, evaluation strategies (e.g., call-by-value, call-by-name) and its Turing completeness. In the second part you learn typed lambda calculi, common type systems in functional languages and the connection between types and logic (Curry–Howard). In the end you can use lambda terms, translate them and prove their properties.

What you will be able to do

• prove fundamental properties of reduction in the lambda calculus
• model common data types and control structures in the lambda calculus
• translate lambda terms and combinators into one another
• derive a principal type for untyped terms
• perform translation between lambda terms and proofs (Curry–Howard)

What the module consists of

• VorlesungDelivery of the course material by the lecturer in interaction with the students
• Übung/TutorialWorking on problems individually or in small groups with tutor support; tasks may be computer-based or written

Teaching method

• Vortrag / dialogische VorlesungPresentation of the material and exchange with the students
• Tutorials with exercisesDeepening the material through practice problems, practical application and tutor assistance