16-20 February 2009
Eindhoven, The Netherlands
============================================================== COURSE ANNOUNCEMENT HIGHLIGHTS of Lambda Calculus and Term Rewriting Systems by Henk Barendregt & Jan Willem Klop. Five day mini-course, Monday February 16 - Friday February 20, 2009, location: Technical University Eindhoven, The Netherlands. Registration: www.win.tue.nl/math/eidma BACKGROUND. Lambda Calculus and Combinatory Logic were instrumental in codifying the fundamental notion of computability, in the days of Goedel, Church, Kleene and Turing. Later on, these formal systems became the heart of functional programming. Typed lambda calculus, with the famous Curry- Howard-de Bruijn isomorphism, became the source of applications in the realm of correctness of formal proofs in mathematics and software, with the aid of proof assistants and theorem provers. At a parallel track, term rewriting systems emerged, of which Lambda Calculus and Combinatory Logic are prominent examples. The development along this line was intertwined with the emergence of the theory of abstract data types. Recently, infinitary versions of both lambda calculus and term rewriting are studied. PROGRAMME (also at www.cs.ru.nl/~henk/LC-TRS.pdf) 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. Day 1. ABSTRACT REWRITING AND TERM REWRITING (a) Newman?s Lemma and Decreasing Diagrams (b) Critical Pair Completion (c) Toyama?s Theorem; modularity (d) Termination via Iterative Path Orders Day 2. LAMBDA CALCULUS AND COMBINATORY LOGIC (a) Computable functions on numbers and data types (b) The fundamental theorems on reduction (c) Combinators and lambda terms (d) Reduction Strategies Day 3. ORTHOGONAL TERM REWRITING (a) The Erasure Lemma (b) Root normal forms (c) Reduction cycles (d) Combinatory Reduction Systems Day 4. TYPED LAMBDA CALCULI (a) Strong normalization of simply typed lambda calculus (b) Type algebras and intersection type structures (c) The Curry-Howard-de Bruijn isomorphism (d) Pure Type Systems Day 5. INFINITARY REWRITING (a) iTRSs and infinitary lambda calculus (b) The infinitary unique normal form property; Boehm Trees (c) Productivity of stream definitions (d) Sequentiality and definability To register as applicant, goto < www.win.tue.nl/math/eidma> . Costs for (PhD) students: 300 Euro; participants of Dutch graduate schools are entitled to 100 Euro reduction. A certificate of attendance will be provided. Further course information can be obtained from the lecturers: jwk@cs.vu.nl, henk@cs.ru.nl. ============================================================