Lean-MLIR: Verified Compilation in Lean

Lean-MLIR

Theory of static single assignment developed in the Lean proof assistant. We also build a wealth of tooling to interact closely with the MLIR compiler ecosystem, to enable workflows that include formal tverification in the day-to-day of MLIR development.

Documentation

• Publication: Verifying Peephole Rewriting In SSA Compiler IRs
• GitHub Repo

Team

• Siddharth Bhat
• Alex Keizer

as well as our scientific collaborator Andres Goens.