Universiteit van Amsterdam

Archives

Institute for Logic, Language and Computation

Please note that this newsitem has been archived, and may contain outdated information or links.

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

Speaker: Henk Barendregt and Jan Willem Klop
Date: 16-20 February 2009
Location: Technical University Eindhoven
Costs: (PhD) students: 300 Euro; members of Dutch graduate school 100 reduction

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.

Please note that this newsitem has been archived, and may contain outdated information or links.