Adventures in Type Theory

5 posts, oldest first

• 1. Adventures in Type Theory 1 — Locally Nameless STLC (Part 1)

  Formalizing the simply-typed lambda calculus using locally nameless representation in Lean 4

  Published 2025-08-24 (Edited 2025-08-26)

• 2. Adventures in Type Theory 2 — Coming in Clutch

  Clutch semantics and continuation-passing style in type-theoretic SSA

  Published 2025-08-25

• 3. Adventures in Type Theory 3 — Scraping By

  Scraping together a formalization of SSA semantics with de Bruijn indices and substitution lemmas

  Published 2025-09-03

• 4. Adventures in Type Theory 4 — The Ship of Thesis

  From SSA to MLIR — building a typed representation of regions, basic blocks, and control-flow graphs

  Published 2025-10-01

• 5. Adventures in Type Theory 5 — Paper Planes

  Recapping our POPL submission on iterative expression languages and sketching region-parameterized extensions

  Published 2025-10-07