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

**Recap**

**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