Content
We study the lambda-calculus both for its logical content and as a key tool to study the semantics of (functional) programming languages.
- We first introduce the simply typed lambda-calculus as a term-like way to represent natural deduction proofs in the minimal fragment of propositional intuitionistic logic, and we establish the Curry-Howard isomorphism (proofs as programs) by showing that normalization in natural deduction corresponds to evaluation in the lambda-calculus.
- We then study the untyped lambda-calculus, some of its operational properties (e.g. confluence, normalization strategies), and the fact that, despite its simplicity, it is a Turing-complete model of computation; in particular, we show how to use the untyped lambda-calculus as a prototypical functional programming language that can model arithmetic, Booleans, data structures, and recursion.
- Finally, we study some type systems (non-idempotent intersection types, system F) for the lambda-calculus that are more flexible and expressive than simple types and can still guarantee that well-typed programs behave well.
Schedule
| week |
date |
topics |
slides |
exercises |
solutions |
|---|
| 01 |
09/10 |
Natural deduction for propositional minimal logic |
pdf (1x1, 4x1) |
pdf |
pdf |
| 02 |
23/10 |
Curry-Howard and the simply typed lambda-calculus |
pdf (1x1, 4x1) |
pdf |
pdf |
| 03 |
30/10 |
Strong normalization of the simply typed lambda-calculus |
|
|
|
| 04 |
06/11 |
The untyped lambda-calculus. Confluence of beta-reduction |
|
|
|
| 05 |
13/11 |
Programming with the untyped lambda-calculus |
|
|
|
| 06 |
20/11 |
Turing-completeness of the untyped lambda-calculus |
|
|
|
| 07 |
27/11 |
Non-idempotent intersection types systems: characterization of head-normalization |
|
|
|
| 08 |
04/12 |
Non-idempotent intersection types: characterization of normalization and strong normalization |
|
|
|
| 09 |
11/12 |
Second-order minimal logic and system F |
|
|
|
| 10 |
18/12 |
Programming with system F. Polymorphism |
|
|
|
| 11 |
08/01 |
Strong normalization of system F |
|
|
|
| 12 |
15/01 |
Recap and revision |
|
|
|
|
22/01 |
Student presentations |
|
|
|
|
29/01 |
Test (written and oral) |
|
|
|
Literature
Slides and solutions to selected exercises will be made available online.
Accompanying literature will be provided.