Week 7: Mathematical Foundations of Proof Assistants (Guest Session)
Overview
Dr. Assaf Kfoury from Boston University will bridge the pragmatic use of Lean with the mathematical theory that makes proof assistants work. Building on prior weeks’ hands-on experience with tactics and functional programming in Lean4, we explore the untyped and simply-typed lambda calculi, the Curry-Howard isomorphism between proofs and programs, and how this relates to proof assistants (and Lean 4, in particular).
Guest Lecturer
- Dr. Assaf Kfoury — Professor of Computer Science (Boston University) | Website
Session Information
- Date and Time: Friday, 13 March, 16:00 — 18:00 (Beirut time)
- Note: The lecture itself is expected to be 16:00 — 17:30, with a 30-minute Q&A session in the end
- Place: Online
- Online Meeting Link (Meeting number: 2404 923 5138; Password: nWzbaGU@324)
- Session Recording (Password: mNDnUp@3)
Core Concepts
Dr. Kfoury will serve as a guide through the material rather than a traditional lecturer; the goal is to illuminate the path from theory to modern proof assistants, and to help students understand how to navigate from introductory to advanced topics on their own.
Dr. Kfoury’s essential goal in this session will be to give a good explanation and justification for the following main results:
The Church-Rosser Property — Confluence of reduction in the lambda calculus
Strong Normalization of the Simply-Typed Lambda Calculus — Every well-typed term reduces to a normal form in finitely many steps, regardless of reduction order (i.e. types rule out non-termination).
The Curry-Howard Isomorphism — Propositions are types, proofs are programs, and proof checking is type checking.
Theoretical Foundations of Proof Assistants (and Lean 4) — How the three results above come together to explain why a system like Lean 4 works: its type theory guarantees that well-typed proof terms are meaningful, terminating, and confluent.
Note: The distributed slides and handouts contain significantly more material than can be covered in a single session. Dr. Kfoury will use the session to orient students within this broader area, indicating which parts to prioritize and how to progress from the accessible to the advanced.
Slides
Week 7 Material (Slides and Handouts):
Note that archive1.zip contains 7 PDF files and one Lean4 file (all of which were composed by Dr. Assaf Kfoury himself), and archive2.zip contains 5 PDF files (the first 4 chapters in the book “Lectures on the Curry-Howard Isomorphism” by Sorensen and Urzyczyn).
Seminar
As part of a large lecture series (with similar themes), Dr. Assaf Kfoury and his colleague Dr. Marco Gaboardi at Boston University have given three lectures titled “What Are Proof Assistants?”, “How To Use Them?”, and “Why Do They Work?”. Their audience was mostly philosophers of mathematics at US institutions on whose initiative they prepared the lectures. The material in these documents overlaps with — without duplicating — the material presented in PROOF101.
Dr. Assaf Kfoury kindly authorized to publicize them and make them available to our students:
Note that the documents provided cover much more material than what they were able to present in the three lectures.
Readings
Dr. Kfoury recommends, among other resources, the following additional references:
Foundational Text:
- J. Roger Hindley — “Basic Simple Type Theory”, Cambridge University Press
More Advanced Papers by Jean-Yves Girard:
Note: These papers are follow-ups to System F and are a bit more difficult to read than Hindley’s book.
Jean-Yves Girard — “Linear Logic” Theoretical Computer Science 50 (1987) 1-102, North-Holland
Jean-Yves Girard — “The System F of Variable Types, Fifteen Years Later” Theoretical Computer Science 45 (1986) 159-192, North-Holland
Navigation
- ← Previous Week: Formalizing Mathematics and Contributing to Mathlib
- Back to Course Overview
- Next Week: Metaprogramming in Lean and Decision Procedures →
Questions? Reach out on the course Discord!