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¶
Team¶
- Siddharth Bhat
- Alex Keizer
as well as our scientific collaborator Andres Goens.