Lambda-Calculus and Type Theory

• ISR 2024, Obergurgl, Austria
• Herman Geuvers and Niels van der Weide, Radboud University Nijmegen, The Netherlands

  Material

  • On Type Theory: Introduction to Type Theory by Herman Geuvers, notes of a summer school course given in Uruguay in 2008.
  • The slides and exercises, please find the pdfs below.
  • Femke van Raamsdonk - Logical Verification Course Notes, Vrije Universiteit Amsterdam, Autumn 2008.
  • M. Takahashi - Parallel Reductions in lambda-Calculus, Information and Computation, Volume 118 (1), 1995, pp. 120-127.
  • Background: 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.
  • Background: The book Type Theory and Formal Proof -- An Introduction (Rob Nederpelt and Herman Geuvers) has appeared in November 2014 with Cambridge University Press.
  • On lambda calculus: Introduction to Lambda Calculus - selected pages by Barendregt and Barendsen. (This is a selection of pages from the full Introduction to Lambda Calculus.)
  • On the Coq Proof Assistant: you may find one of the following useful:
    • A short and convenient cheatsheet with a list of useful Coq tactics.
    • A slightly longer convenient cheatsheet with a list of useful Coq goodies by Jules Jacobs.
    • Coq in a Hurry by Yves Bertot. A quick introduction to Coq, notably read Section 3.
    • A short introduction to Coq by the developers.
    • The starting page for Coq documentation.

  Schedule

  • Monday
    • lecture 1. Introduction, syntax and operational semantics of untyped lambda calculus
    • lecture 2. Simple type theory, formulas-as-types and proofs-as-terms
    • lecture 3. First order dependent type theory, formulas-as-types and proofs-as-terms
    • exercises day 1 and some answers.
  • Tuesday
    • lecture 4. Coq: proposition logic and predicate logic, interactive theorem proving using tactics
      You can install Coq or use it in your browser
    • lecture 5. Coq: inductive types
    • exercises 2: Work on the Coq exercises or the exercises of day 1
    • lecture 6. Polymorphic types
  • Wednesday
    • lecture 7. Higher order logic in the Calculus of constructions and in Coq
    • exercises day 3; the ones for lecture 7 can also be done in Coq using the HOL_inductivetypes.v file and some answers.
    • lecture 8. Simple meta theory of type systems and type checking algorithm
    • lecture 9. Church-Rosser property
  • Friday
    • exercises day 4 and some answers.
    • lecture 10. Weak normalization and strong normalization property
    • lecture 11. Normalization by evaluation.
    • exercises day 5 and some answers.
  • Saturday
    • lecture 12. Principal types: a functional programmers' view on type theory
    • lecture 13. Homotopy type theory.
    • Some exercises day 6 about lecture 12; the content of lectures 12 and 13 will not be part of the test, so you can also this as a question session for the test.
    • Test: test.pdf file, please write your answers on paper and hand in. You can make exercises 7 and/or 8 in Coq: please complete this Coq file and send it to herman@cs.ru.nl and nweide@cs.ru.nl

  ---

  herman at cs dot ru dot nl