Blog

• Adventures in Type Theory 5 — Paper Planes

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

  Published 2025-10-07

• 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

• 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

• Adventures in Type Theory 2 — Coming in Clutch

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

  Published 2025-08-25

• 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)

• Building An Inductive Representation of SSA

  Constructing an inductive representation of static single assignment form suitable for mechanized metatheory

  Published 2024-07-21

• Fun with Sentence Embedding

  Using sentence embeddings for clustering, topic modelling, and classification of text datasets

  Published 2023-10-08 (Edited 2024-06-04)

• What Makes a Language Fast?

  Exploring how language design choices affect runtime performance through benchmarks and low-level analysis

  Published 2023-08-18 (Edited 2024-05-10)