Abstract:

Dependent Type Theory is a formal language mixing logic and computation, at the basis of proof assistants and programming languages such as Agda, Coq, Idris and Lean. It took its roots in the type theories of Russell, Church and the theory of typed lambda-calculi to become, under the impulse of de Bruijn, Martin-Löf and others, a foundation for formalized mathematics and the mechanized verification of proofs and programs. In this course we will review the history and development of dependent type theory and focus on its theoretical foundations, that is:

1. Untyped and typed lambda calculi: Confluence and termination properties

2. The Curry-Howard correspondence: Linking typed λ-calculi and logics

3. Pure Type Systems: From simply-typed λ-calculus to F-omega to the Calculus of Constructions

4. Dependent Type Theories: Martin-Löf type theories and the Calculus of Inductive Constructions

The course material is available at https://www.irif.fr/~sozeau/teaching/TYPES18.en.html.