24Compilers, Kernels & Language Implementations
23 entries
- lean4leanLean 4 kernel written in Lean 4.digama0/lean4lean
- nanodaIndependent Lean 4 type checker written in Rust.ammkrn/nanoda_lib
- con-lecheExternal Lean checker with a consistency proof (con-ron is a Rust port proved with Aeneas).leanprover/con-leche
- MetaleanVerified type checker for an idealized Lean type theory.intgrah/metalean
- Lean4LessTranslates Lean into smaller theories by eliminating definitional equalities.Deducteam/Lean4Less
- lean2agdaExports elaborated Lean code to Agda.lyphyser/lean2agda
- thalesTypeScript compiler and JavaScript engine in Lean.jessealama/thales
- leanexeCompiler for a Lean dialect that targets verified WebAssembly.jsmorph/leanexe
- lean2wasmCompile Lean to WebAssembly.T-Brick/lean2wasm
- lean-virProof of concept compiling Lean IR to wasm32-wasi.ejgallego/lean-vir
- lean-gccjitBindings to libgccjit, a basis for alternative backends.SchrodingerZhu/lean-gccjit
- QED64Lean and Mathlib running in the browser via wasm64.FawadHa1der/QED64
- yatimaZero-knowledge Lean 4 compiler and kernel.argumentcomputer/yatima
- ixZero-knowledge proof-carrying code for Lean 4.argumentcomputer/ix
- mm-lean4High-performance Metamath verifier.digama0/mm-lean4
- SomaDependently typed language powered by interaction nets.SrGaabriel/soma
- lapisConcurrent Language Server Protocol framework.SrGaabriel/lapis
- qdtQuery-based dependent type elaborator.intgrah/qdt
- DeBruijnSSAFormalization of SSA.imbrem/debruijn-ssa
- verified-compilerToy verified compiler.marcusrossel/verified-compiler
- LyreWrite Lean IR as Lean syntax.tydeu/lyre
- LRTModel of Lean's runtime primitives in Lean, partly porting the C runtime (work in progress).tydeu/lrt
- LeanPyExperimental implementation of Python in Lean.tydeu/leanpy