Foundations of formalised mathematics and higher-dimensional rewriting

ENS de Lyon, Autumn 2024

Lecturer: Georg Struth, University of Sheffield


News

  • 02.12.24 second exercise sheet published
  • 26.11,24 the lectures on Thu Nov 28, 10-12 have been rescheduled to Fri Nov 29, 14-16 in Seminar Room 2
  • 25.11.24 exam dates and modalities announced
  • 24.11.24 introductory Isabelle theories uploaded
  • 24.11.24 first exercise sheet published
  • 17.11.24 published course website

Overview

This course is part of the Master 2 Programme Higher Algebra and Formalised Mathematics at ENS de Lyon The course consists of two parts of around one week each.

Type theory

This first part introduces the foundations of the dependent type theories that forms the backbone of proof assistants like Coq or Lean. After a brief review of the untyped λ-calculus and intuitionistic propositional logic, we study the simply typed λ-calculus and the proposition-as-types principle. We then proceed to more expressive type theories leading to the calculus of constructions.

Beyond proof assistants, type theory is also relevant as a foundation of mathematics and as a semantics of programming languages, in particular of functional programming languages. Yet this is beyond the scope of these lectures.

Higher-Dimensional Rewriting

The second part of this course presents ongoing research on applications of higher algebras in higher-dimensional rewriting and the use of proof assistants in their development. To this end, we work with the Isabelle/HOL proof assistant, which is based on a simply-typed classical higher-order logic. We use it mainly to showcase the benefits of proof automation and counterexample generation in formalised mathematics. This part of the course will end with an outline of a larger programme on the formalisation of higher-dimensional rewriting in particular and higher categories in general.

Important Task: Install Isabelle on your machine in the first week (it's really easy!).


Exercises


Assessment

The assessment of this course is based on the solutions of exercises (30%) and a final exam (70%). The final exam will take place on 12.12.2024, 9:00-12:00, salle 125. It will be an open book exam. More information will be given at the end of this course.


Literature

The type theory part of this course is based on two textbooks:
  • Rob Nederpelt and Herman Geuvers, Type theory and formal proof, Cambridge University Press, 2014
  • Morten Heine Sørensen and Paweł Urzyczyn, Lectures on the Curry-Howard isomorphism, Elsevier, 2006
More compact overviews of the subject can be found here: The second book also features an introduction to homotopy type theory.

For information about the type theories underlying Coq, Lean and Isabelle, beyond the material taught in this course, see
  • Yves Bertot and Pierre Castéran, Interactive theorem proving and program development, Coq'Art: the calculus of inductive constructions, Springer, 2004
  • Christine Paulin-Mohring, Introduction to the Calculus of Inductive Constructions, HAL Research Report, 2014
  • Mario Carneiro, The type theory of Lean, 2019
  • M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic, Cambridge University Press, 1993
  • Ondřej Kunčar and Andrei Popescu, A consistent foundation for Isabelle/HOL, J Autom Reason, 2919
Here are two standard textbooks on applications of type theory in program semantics:
  • Robert Harper, Practical foundations for programming languages Cambridge University Press, 2016
  • Benjamin Peirce, Types and programming languages, MIT Press, 2002
Two more influential texts on type theory are
  • Per Martin-Löf, Intuitionistic type theory, 1984
  • Jean-Yves Girard, Yves Lafont and Paul Taylor, Proofs and Types, Cambridge University Press, 1990
Finally, two classical books on categories and types are
  • J. Lambek and P. J. Scott, Introduction to higher order categorical logic, Cambridge University Press, 1986
  • Bart Jacobs, Categorical logic and type theory, Elsevier, 1999
A comprehensive documentation of Isabelle/HOL can be found here: The discussion of higher algebras for higher-dimensional rewriting is based on the following articles:
  • Cameron Calk, Éric Goubault, Philippe Malbos and Georg Struth Algebraic coherent confluence and higher globular Kleene algebras Log. Methods Comput Sci, 2022
  • Cameron Calk, Philippe Malbos, Damien Pous and Georg Struth, Higher catoids, higher quantales and their correspondences, 2023
  • Philippe Malbos, Tanguy Massacrier and Georg Struth Single-set cubical categories and their formalisation with a proof assistant, J Autom Reason, 2024
The Isabelle theories for these structures can be found in the Archive of Formal Proofs: For general references about higher-dimensional rewriting I refer to other courses in this programme and this book.


Isabelle theories

Links