Adventures in Type Theory 5 — Paper Planes
Recapping our POPL submission on iterative expression languages and sketching region-parameterized extensions
tekne.dev
Blog by Jad Ghalayini
Latest posts
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
Adventures in Type Theory 3 — Scraping By
Scraping together a formalization of SSA semantics with de Bruijn indices and substitution lemmas
Adventures in Type Theory 2 — Coming in Clutch
Clutch semantics and continuation-passing style in type-theoretic SSA
Adventures in Type Theory 1 — Locally Nameless STLC (Part 1)
Formalizing the simply-typed lambda calculus using locally nameless representation in Lean 4
Building An Inductive Representation of SSA
Constructing an inductive representation of static single assignment form suitable for mechanized metatheory
Fun with Sentence Embedding
Using sentence embeddings for clustering, topic modelling, and classification of text datasets
What Makes a Language Fast?
Exploring how language design choices affect runtime performance through benchmarks and low-level analysis