ISR 2024
Track B
Track B
schedule material

ISR 2024 – Track B

Lambda-Calculus and Type Theory


This site provides supporting material for Track B of ISR 2024, the 14th International School on Rewriting.


Lecturers


Herman Geuvers Radboud University Nijmegen
Niels van der Weide   Radboud University Nijmegen

Content


The course provides an introduction to type theory and lambda calculus. Lambda calculus is the underlying computational model for functional programming and typed lambda calculus forms the basics of various proof assistants (e.g. Coq) via the so called "formulas-as-types" interpretation where a formula is interpreted as a type and a proof as a term, a "proof term". A proof assistant is an implementation of type theory that allows the user to interactively create a proof term of a given type, that is: to interactively prove a theorem. The terms of type theory are lambda terms, and so type theory also includes a small functional programming language. This combination provides both a very powerful system for doing logic and formalizing mathematics, and a system for programming and proving properties about programs. The reliability of a type theory based proof assistant crucially relies on the decidability of type checking (= proof checking). For this many deep properties have to be proven for the type theory.


The following topics will be treated: syntax and operational semantics of untyped lambda calculus; simple type theory; first order dependent type theory; formulas-as-types and proofs-as-terms; inductive types, polymorphic types; calculus of constructions; the type theory of Coq; simple meta theory of type systems; type checking algorithm; Church-Rosser property; normalization property; normalization by evaluation. We will also introduce the Coq proof assistant and allow the students to get some hands on experience with it. Finally, we will provide a brief outlook on how functional programmers view type theory and on homotopy type theory.


The course consists of 20 slots of 90 minutes: 13 lecture slots, 6 exercises sessions, and a final test (for students requiring an ECTS certificate).


Prerequisites