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

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:

1. The Church-Rosser Property — Confluence of reduction in the lambda calculus

2. 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).

3. The Curry-Howard Isomorphism — Propositions are types, proofs are programs, and proof checking is type checking.

4. 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):

Download Archive 1

Download Archive 2

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).

Readings

Dr. Kfoury recommends, among other resources, the following additional references:

Foundational Text:

• J. Roger Hindley — “Basic Simple Type Theory”, Cambridge University Press
  Contact Daniel Dia to obtain the PDF.

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
  Contact Daniel Dia to obtain the PDF.

• Jean-Yves Girard — “The System F of Variable Types, Fifteen Years Later” Theoretical Computer Science 45 (1986) 159-192, North-Holland
  Contact Daniel Dia to obtain the PDF.

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!