This repository has course materials (lecture slides, labs, and an assignment) for a course I taught in 2025 on logic, lambda calculus, and type theory.
I wanted to understand the equation "proofs = programs" so, naturally, I taught a course on the related ideas.
I covered Gentzen's natural deduction, Peano arithmetic, untyped lambda calculus, and simply type theory. In the final lectures and assignment I gave an introduction to the proof assistant Lean. Explaining how the logic and type theory from earlier in the course have led to the development of tools like Lean.