Taught by Henk Barendregt and Freek Wiedijk
Assisted by Andrew Polonsky

Organized by Mastermath

Period 06.02-21.05, 2012, Monday afternoon
Lecture 14:00-14:45 and 16:00-16:45
Exercises 15:00-15:45
Location Minnaert Building 205, Leuvenlaan 4, Uithof, Utrecht
(on 27.2 Buys Ballot Lab 071, Princetonplein 5).

Untyped lambda calculus
06.2 Combinatory logic and lambda calculus and exercises.
13.2 Computability, Church-Rosser theorem and exercises.
20.2 Coding terms and exercises.
27.2 Boehm Trees and exercises.

Typed lambda calculus
05.3 Simply typed lambda calculus and exercises.
12.3 Dependent types & pure type systems and exercises.
19.3 Higher order lambda calculus and exercises.
26.3 Inductive types and exercises. Answers


02.4 Recap and test. Answers.

Typed lambda calculus for mathematics
16.4 Introduction to Coq
23.4 The next generation of proof-checkers

Advanced topics in lambda calculus
07.5 Strong Normalization
14.5 The canonical term models and exercises.
21.5 Inconsistencies

Exam (including answers)                              Resit
June 4, 13:30-16:30                                         June 25, 13:30-16:30
EDUCATORIUM BETAZAAL                       BBL 007