@mattpd

690 Followers
668 Following
1.2K Posts

"Practical Formal Verification for MLIR Programs"

https://arxiv.org/pdf/2605.01124

Really happy to see stuff happening in e-graphs. From a university in Switzerland nontheless!

Versioned E-Graphs
https://programming-group.com/assets/pdf/papers/2026_Versioned-EGraphs.pdf
from PLDI26

Great paper: The Calculated Typer, by Garby, Bahr, and Hutton
https://pca.st/rqqgrxpt
Iowa Type Theory Commute Podcast S7 E6 by Aaron Stump
Great paper: The Calculated Typer

I discuss a nice paper I quite enjoyed reading, called The Calculated Typer, by Garby, Bahr, and Hutton.  The authors take a very nice general look at the specification of a type checker, for a very…

Pocket Casts

Gluon and Linear Layouts Deep-Dive
Tile-Based GPU Programming with Low-Level Control
Video: https://www.youtube.com/watch?v=oYs_qtuk2Pg
Slides: https://github.com/gpu-mode/lectures/tree/main/lecture_104
GPU MODE Lecture 104; April 22, 2026
Keren Zhou, Peter Bell, Mario Lezcano
Hosted by Mark Saroufim

Topics:
- Gluon: https://triton-lang.org/main/gluon/ - optimized Blackwell Matmul, tutorials & examples
- Proton: Towards Multi-level, Adaptive Profiling for Triton: https://doi.org/10.1109/CGO68049.2026.11395207
- Sanitizers
- Linear Layout Visualizer: https://deep-learning-profiling-tools.github.io/linear-layout-viz/

https://yangzhixuan.github.io/NbE.html

My (rather long) blog post on normalisation by evaluation is online now. In this post I show how we can optimise a naive substitution-based applicative-order normaliser of untyped calculus step by step, leading us to reconstruct NbE as "weak-applicative-order normalisation with meta-level laziness, lazy substitution, and de Bruijn levels". We will also examine some "adversarial exploit" that makes NbE slow and use the insights gained from our reconstruction of NbE to optimise NbE.

An Algorithmic Reconstruction of Normalisation by Evaluation

How To Make a Fast Dynamic Language Interpreter
https://zef-lang.dev/implementation
by Filip Jerzy Pizło
How To Make a Fast Dynamic Language Interpreter

Oh nice, a new variant of SSA for directly encoding closures and higher-order functions just dropped https://arxiv.org/abs/2604.09961
SSA without Dominance for Higher-Order Programs

Dominance is a fundamental concept in compilers based on static single assignment (SSA) form. It underpins a wide range of analyses and transformations and defines a core property of SSA: every use must be dominated by its definition. We argue that this reliance on dominance has become increasingly problematic -- both in terms of precision and applicability to modern higher-order languages. First, control flow overapproximates data flow, which makes dominance-based analyses inherently imprecise. Second, dominance is well-defined only for first-order control-flow graphs (CFGs). More critically, higher-order programs violate the assumptions underlying SSA and classic CFGs: without an explicit CFG, the very notion that all uses of a variable must be dominated by its definition loses meaning. We propose an alternative foundation based on free variables. In this view, $ϕ$-functions and function parameters directly express data dependencies, enabling analyses traditionally built on dominance while improving precision and naturally extending to higher-order programs. We further present an efficient technique for maintaining free-variable sets in a mutable intermediate representation (IR). For analyses requiring additional structure, we introduce the nesting tree -- a relaxed analogue of the dominator tree constructed from variable dependencies rather than control flow. Our benchmarks demonstrate that the algorithms and data structures presented in this paper scale log-linearly with program size in practice.

arXiv.org
Fundamentals of CuTe Layout Algebra and Category-theoretic Interpretation
https://www.youtube.com/watch?v=MVh_guNbWMA
https://github.com/gpu-mode/lectures/tree/main/lecture_103
GPU MODE Lecture 103; Apr 18, 2026
Jack Carlisle & Jay Shah
Hosted by Mark Saroufim & Cris Cecka
Lecture 103: Fundamentals of CuTe Layout Algebra and Category-theoretic Interpretation

YouTube
A simplified model of Fil-C

Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)
https://arxiv.org/abs/2602.20082
https://zoep.github.io/blog/2026/04/17/machine-generated-code-machine-checked-proofs/
by Zoe Paraskevopoulou
Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)

We report on using an agentic coding assistant (Claude Code, powered by Claude Opus 4.6) to mechanize a substantial Rocq correctness proof from scratch, with human guidance but without human proof writing. The proof establishes semantic preservation for the administrative normal form (ANF) transformation in the CertiCoq verified compiler for Rocq. The closely related continuation-passing style (CPS) transformation in CertiCoq was previously proved correct by human experts over several months. We use this proof as a template and instruct the LLM to adapt the proof technique to the ANF setting, which differs in important technical ways. The resulting ANF proof comprises approximately 7,800 lines of Rocq (larger than the 5,300-line CPS proof) and was developed in approximately 96 hours. We describe the proof technique and report on the experience of developing it with an LLM, discussing both the strengths and limitations of the approach and its implications for verified compiler construction.

arXiv.org