λ-calculus
| Femke van Raamsdonk (VU University Amsterdam) |
Slides of lecture 1 and lecture 2.
The λ-calculus is originally introduced by Church to study the foundations of mathematics. λ-terms with β-reduction form a Turing-complete model of computation. In this course we will discuss some subjects in the rewriting theory of λ-calculus. Every lecture will have the following structure: lecture, time to work individually on a few exercises, wrap-up.
The first lecture is concerned with the basics of λ-calculus: terms, terms modulo α, β-reduction, and an introduction to reduction strategies and confluence of β-reduction.
In the second lecture we will discuss the expressivity of λ-calculus, in particular the encoding of data types and recursive functions.
The third lecture will be mainly concerned with the standardization theorem.
Finally we will turn to the simply typed λ-calculus, and discuss a proof that β-reduction is terminating on simply typed terms.