ISR 2026 — 15th International School on Rewriting

Advanced Track lecturers: Herman Geuvers

Weak and strong normalization for typed lambda calculus

The course describes methods to prove weak and strong normalization for Type Theory, notably we will discuss the proof of weak normalization for simple type theory due to Turing (first published by Gandy) and the well-known "reducibility candidates" method (also known as "saturated sets") originally due to Tait and extended by Girard to polymorphic and hiher order systems. The latter method has become a general proof technique for proving strong normalization and we will indicate how widely applicabale it is. We will start of with introducing the problem of normalization in te context of powerful dependent type theories, like the ones implemented in the proof assistant Rocq (and Lean and Agda) and the role it plays in the type checking algorithm and the soundness of the system.

Materials

• slides of lectures
• H. Geuvers - Introduction to Type Theory, in Language Engineering and Rigourous Software Development (Revised Tutorial Lecture Notes of LerNet ALFA Summer School Piriapolis, Uruguay, 24 February to 1 March, 2008), eds.: Ana Bove, Luis Soares Barbosa, Alberto Pardo, Jorge Sousa Pinto, LNCS 5520, Springer 2009.

Background material

1. H. Barendregt and H. Geuvers - Proof Assistants using Dependent Type Systems, Chapter 18 of the Handbook of Automated Reasoning (Vol 2), eds. A. Robinson and A. Voronkov, Elsevier 2001, pp. 1149 -- 1238.
2. Rob Nederpelt and Herman Geuvers - Type Theory and Formal Proof, An Introduction, Cambridge University Press, December 2014.