16-20 February 2009, Mini-course Highlights of Lambda Calculus and Term Rewriting Systems

This five day master class in lambda calculus and term rewriting is centered around some twenty of the main theorems, both classical and recent. Each theorem is treated in a syllabus chapter of 10 pages, concluded with a section of exercises and notes for follow-up subjects and further reading.

Preliminary program

Day 1. ABSTRACT REWRITING AND TERM REWRITING

1. Newman's Lemma and Decreasing Diagrams
2. Critical Pair Completion
3. Toyama's Theorem; modularity
4. Termination via Iterative Path Orders

Day 2. LAMBDA CALCULUS AND COMBINATORY LOGIC

1. Computable functions on numbers and data types
2. The fundamental theorems on reduction
3. Combinators and lambda terms
4. Reduction Strategies

Day 3. ORTHOGONAL TERM REWRITING

1. The Erasure Lemma
2. Root normal forms
3. Reduction cycles
4. Combinatory Reduction Systems

Day 4. TYPED LAMBDA CALCULI

1. Strong normalization of simply typed lambda calculus
2. Type algebras and intersection type structures
3. The Curry-Howard-de Bruijn isomorphism
4. Pure Type Systems

Day 5. INFINITARY REWRITING

1. iTRSs and infinitary lambda calculus
2. The infinitary unique normal form property; Boehm Trees
3. Productivity of stream definitions
4. Sequentiality and definability

Deadline for registration is January 30th, 2009. For more information, see http://www.win.tue.nl/math/eidma/courses/minicourses/barendregtenklop/. The complete programme may be found at http://www.cs.ru.nl/~henk/LC-TRS.pdf.