Projects¶

Lean-MLIR: Verified Compilation in LeanFormal verification for the LLVM and MLIR compiler ecosystem, at scale.High-Productivity Compiler DevelopmentMaking compiler design accessible, with xDSL and declarative IR definitions.Open-Source Electronic Design AutomationAn open ecosystem for FPGA and ASIC design, simulation, and verification.Seamless Design of Smart Edge ProcessorsA compiler toolchain for low-power AI accelerators at the edge.Compilation for Quantum ComputersCompiler technology for an open-source quantum computing ecosystem.FPL: A Fast Presburger LibraryFast Presburger arithmetic for loop optimization, upstream in MLIR.

Earlier Projects¶

• Polly (lead developer)
  High-Level Optimizer for LLVM
• Graphite (reviewer)
  High-Level Optimizer for GCC
• isl (contributor)
  An integer set library
• islplot
  Visualization library for integer sets
• ppcg (contributor)
  C to CUDA/OpenCL compiler
• clang_complete
  Vim C++ code completion
• Dr. Cube
  J2ME Rubik's Cube simulator