Johannes' blog

Ramblings about my research and "academic life."

See the News section for announcement-style posts.

Small Inversions for Proof Irrelevance

Elegantly proving that your Rocq predicate is proof-irrelevant with one weird trick

23 min read · June 30, 2026

2026 · rocq small-inversions
Tree Borrows: A Model of LLVM's noalias?

Accidentally defining an aliasing model for LLVM

18 min read · November 18, 2025

2025 · tree-borrows noalias llvm
My Experience Attending OPLSS’25

What is the Oregon Programming Language Summer School like?

18 min read · July 15, 2025

2025 · oplss travel