Week 3: Dependent Types Part 1

Overview

We motivate the entire audience (especially software engineers and mathematicians) by showing the catastrophic failures of “correct-looking” code. Through a couple compelling case studies, including the Ariane 5 rocket explosion, the Therac-25 radiation machine, and the Heartbleed bug, we’ll examine the limits of testing and introduce the concept of formal verification as a path to (almost*) truly reliable software.

Lecturer

  • Daniel Dia — Course creator, primary instructor & organizer (American University of Beirut); Computer & Communications Engineering (CCE) and Mathematics dual-degree student (AUB).

Session Information

Core Concepts

  • Lambda calculus foundations: λ-abstraction syntax (λx. M), β-reduction (function application), α-conversion (variable renaming), Church encodings (booleans, numerals as functions), higher-order functions (twice, compose), currying (multiple arguments as nested functions)
  • Simply typed lambda calculus: adding types for safety, type checking and inference, type judgments, function types, why types matter (catch errors, documentation, optimization)
  • Curry-Howard correspondence: programs ↔ proofs, types ↔ propositions, → ↔ ⟹, × ↔ ∧, + ↔ ∨, ∀ as dependent functions, type checking = proof checking
  • Types in Lean: basic types (Nat, Int, Bool, String), function types (right-associative), type constructors (List), product types (×), sum types (+), Option types (fixing null pointers), polymorphism with type variables
  • Inductive types: natural numbers (Peano: zero, succ), lists (nil, cons), binary trees (empty, node), pattern matching, structural recursion (guaranteed termination), “no junk, no confusion” principle
  • Dependent types: types depending on values (Vector α n, Fin n for bounded numbers, subtypes {x : α // P x}), dependent function types (Π-types), Barendregt’s λ-cube (four corners of type dependencies)
  • Lean’s architecture: elaborator (untrusted, fills implicits/tactics) vs kernel (trusted ~10k lines, type checks all terms), De Bruijn criterion (small trusted core), De Bruijn indices (variables as numbers, no alpha-conversion needed)

Slides

Week 2 Slides: Download PDF

Readings

  1. Theorem Proving in Lean 4 (Chapters 1-2-3)
  2. Optional: Functional Programming in Lean 4 (Chapter 7)
  3. The Hitchhiker’s Guide to Logical Verification (Chapters 1-2)
  4. Good YouTube video for intuition: “Type theory and the algebra of types” by All Angles

Additional References

For students interested in deeper foundations of type theory, 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 2: Types and Type Inference

Quiz Link: Take Quiz 3

Deadline: Before Week 3 session
Passing Score: 60%

Programming Assignment

Assignment 2: Types and Functions in Lean

Objective: Practice working with Lean’s type system and write your first functions.

Assignment: PROOF101 Programming Assignment 2

Questions? Reach out on the course Zulip!