Week 7: Mathematical Foundations of Proof Assistants (Guest Session)

Overview

This session bridges the pragmatic use of Lean with the deep mathematical theory that makes proof assistants work. Building on prior weeks’ hands-on experience with tactics and functional programming in Lean4, we explore the type-theoretic foundations, the Curry-Howard isomorphism between proofs and programs, and algorithms for type inhabitation and counting.

Guest Lecturer

• Dr. Assaf Kfoury — Professor of Computer Science (Bostob University)

Session Information

• Date and Time: Monday 2 March, 15:00 — 17:00 (Beirut time)
• Place: IOEC (Oxy) 518
• Online Meeting Link
• Recording

Core Concepts

• TBD

Slides

Week 7 Slides: Download PDF

Readings

Dr. Assaf Kfoury (Boston University) recommends the following 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.

Weekly Quiz

Quiz 7: Type Theory and Proof Assistants

Quiz Link: Take Quiz 7

Deadline: Before Week 8 session
Passing Score: 60%

Navigation

• ← Previous Week: Contributing to Mathlib
• Back to Course Overview
• Next Week: Monads, Tactics, and Applications →

Questions? Reach out on the course Discord!