Week 2: Dependent Types

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

• Date and Time: Monday 26 January, 15:00 — 17:00 (Beirut time)
• Place: IOEC (Oxy) 518
• Online Meeting Link (Meeting number: 2408 255 0026; Password: 2ckMp3FJ58*)
• Recording (Password: 7GkasQg*)
• Additional Recording (covering everything we could not during the lecture)

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. Functional Programming in Lean 4 (Chapter 7)
3. The Hitchhiker’s Guide to Logical Verification (Chapters 1-2)

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 2

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

Navigation

• ← Previous Week: Why Our Code Breaks
• Back to Course Overview
• Next Week: Thinking Functionally →

Questions? Reach out on the course Discord!