Dependable Types

A mini-series introduction to lambda calculus, a deep dive into dependent types, and a love letter to Idris.

  1. Full-STλC Development
  2. Correctness by Construction
  3. Reductio Sine Absurdum
  4. Terms Are Types Are Terms