Masterclass Typed Lambda Calculus

by Henk Barendregt assisted by Wil Dekkers and Venanzio Capretta

Fall Semester 2006, Wednesdays 10.00-13.00.

Radboud University, Huygens Building 3.054,

Toernooiveld 1, Nijmegen

Behind the content of the lectures the numbers refer to the references below.

20.09.2006 Week 1 Excercises

Untyped theory: conversion, reduction, Church numerals, A_+, A_*, A_exp. (5: Sct. 2.2).

Typed theory: Typing a la Curry (1: Ch. 5; 2: Sct. 1.1).

27.09.2006 Week 2 Excercises

Untyped theory: Representing arbitrary computable functions (5: Sct. 2.2). Fixed-points. (5: Sct. 2.1.)

Typed theory: Typing algorithm. (2: 2.3.6-2.3.16; it is less difficult than it looks!)

Inhabitation algorithm for typing a la Curry (2: Sct. 1.2).

04.10.2006 Week 3 Excercises

Untyped theory: eta-reduction (2: 1.1.5). Coding and reflection (4: Sct. 5).

Typed theory: eta-expansion (2: Sct. 1.2).

11.10.2006 Week 4 test 1

Untyped theory: second fixed-point theorem (6: Thm. 6.5.9), Scott's theorem (6: Thm. 6.6.2);

Church-Rosser theorem (1: Ch 4).

Typed theory: Church typed terms. (2: Sct 1.1).

18.10.2006 Week 5 Excercises

(Un)typed theory: Proof of the Church-Rosser theorem. (1: Ch. 4).

Typed theory: Generation Lemma; Subject reduction (2: 2.1).

25.10.2006 Week 6 Excercises

(Un)typed theory: lambda-I-calculus (6: Sct 2.2), strong normalization (6: Def. 3.1.22), head nf. (6: Def. 8.1.7-9)

Typed theory: Intersection types. Systems K, CD and BCD (3: Exc. 15.5.2, Sct 15.1, 15.2, Ch 14).

01.11.2006 Week 7 Excercises

Typed theory: Intersection types; filters; models. (3: Ch. 14, CH. 15, Ch. 16).

15.11.2006 Week 8 test 2

Continuation of last week. (3: Selection from Ch. 17, Selection from Ch. 18).

22.11.2006 Week 9 Exercises

Continuation of last week.

29.11.2006 Week 10 Exercises

Final about filter models. Reducibility between simple types (2: Section 3.4).

06.12.2006 Week 11 Exercises

Reduction of types to the top-type (0->0->0)->0->0.

13.12.2006 Week 12 test 3

The hierarchy of types under reducibility.

Reserach problems.

References

1. Introduction to Lambda Calculus. Lecture notes Barendregt-Barendsen.

2. Simply Typed Lambda Calculus Forthcoming book on typed lambda calculus, Part I.

3. Lambda Calculus with Intersection Types Forthcoming book on typed lambda calculus, Part III.

4. Reflection and its use, with an emphasis on lambda calculus Lambda calculus for biologists.

5. Untyped Lambda Calculus Lambda calculi with types, HBK of Logic in Computer Science II.

6. The Lambda Calculus, Its Syntax and Semantics, Elsevier, 1984.