Pinned Repositories
C-parsing-for-Lean4
A parser for ANSI C, in Lean4.
dyn-dialect
A repository to test dialects defined dynamically.
egg-tactic-code
lean-gap
An embedding and formalization of GAP (groups, algorithms, Programming) in LEAN4
lean-mlir
A minimal development of SSA theory
lean-mlir-old
embedding MLIR in LEAN
mlir-fuzz
A enumerator for MLIR, relying on the information given by IRDL.
paper-template
A template for writing CS papers with latex -- includes CI, todonotes, ...
QMLIR
A prototype of an SSA-based quantum IR exploiting value semantics
smt-dialect
An SMT dialect for MLIR, to represent SMTLib programs. And tools to interact with SMT solvers.
opencompl's Repositories
opencompl/lean-mlir
A minimal development of SSA theory
opencompl/lean-mlir-old
embedding MLIR in LEAN
opencompl/paper-template
A template for writing CS papers with latex -- includes CI, todonotes, ...
opencompl/C-parsing-for-Lean4
A parser for ANSI C, in Lean4.
opencompl/mlir-fuzz
A enumerator for MLIR, relying on the information given by IRDL.
opencompl/QMLIR
A prototype of an SSA-based quantum IR exploiting value semantics
opencompl/Quidditch
IREE compiler and runtime for Snitch
opencompl/xdsl-smt
The implementation of an SMTLib dialect for xDSL
opencompl/prover-shootout
Shootout between different proof tools on hard verification problems
opencompl/sail-lean
opencompl/alive
Alive: Automatic LLVM's Instcombine Verifier
opencompl/lean4
Lean 4 programming language and theorem prover
opencompl/lean4-metaprogramming-book
opencompl/lean4web
The Lean 4 web editor
opencompl/llvm-project
The LLVM Project is a collection of modular and reusable compiler and toolchain technologies. Note: the repository does not accept github pull requests at this moment. Please submit your patches at http://reviews.llvm.org.
opencompl/pyluks
opencompl/benchmark-vm
opencompl/BibtexQuery
A simple command-line bibtex query utility written in Lean 4
opencompl/doc-gen4
Document Generator for Lean 4
opencompl/equational_theories
A project to map out the relations between different equational theories of Magmas.
opencompl/falcon-bullseye
BullsEye: A Scalable cache miss calculator for affine programs
opencompl/lazystack-barvinok
Barvinok modified for lazystack
opencompl/lazystack-isl
opencompl/leaff
Leaff is a diff tool for Lean environments
opencompl/lean-mlir-common
Common datastructures for working with MLIR in Lean
opencompl/mathlib4
The math library of Lean 4
opencompl/metaocaml_test
Testing things in metaocaml
opencompl/riscv-isa-sim
Spike, a RISC-V ISA Simulator
opencompl/std4
Standard Library for Lean 4
opencompl/tablegen-stats
Converting tablegen to IRDL, and analyzing it