Stories by matt_d

Lean: Postmortem for the Kernel Soundness Bug Hunt

Portability of Fortran's 'do concurrent' on GPUs II

tmp.0ut Volume 5 – 2026-08

Formal Perf. and Compile Time Guarantees for Compiler Optimization Heuristics

Vero: Can AI Agents Build Formally Verified Software Repositories?

Compile-Time Improvements in LLVM 23

Programming Language Semantics and Memory Safety

Pitfalls of Benchmarking on Modern Systems

Hawkeye: Hardware-Aware GPU Kernel Optimization with Minimal Supervision

Context-Aware Inlining: Using Call-Stack Profiles for Fast and Smaller Binaries

Succinct and Fast Tiny Pointer Hash Tables

Cost-Aware Optimization for Agentic Query Execution

Composing CRDTs Convergent by Construction

LoCalMem: Type-Directed Adaptive Serialization for LAM & CAM

InstrSem: Automatically Inferring Semantics of (Undocumented) CPU Instructions

λλ: A Programming Language for Silicon Photonics

Palomar: A registry of Lean verified mathematics

Memory Allocation for Constant-Bounded Programs

Programmable Property-Based Testing

How to Parallelize a Transformer for Training

1 2 3 4 5 6 7 8 9 10