opencompl

Pinned Repositories

C-parsing-for-Lean4
A parser for ANSI C, in Lean4.
Language:C20 4 63
egg-tactic-code
Language:Lean16 6 01
lean-gap
An embedding and formalization of GAP (groups, algorithms, Programming) in LEAN4
Language:GAP16 4 00
lean-mlir
A minimal development of SSA theory
Language:Lean197 4 12823
lean-mlir-old
embedding MLIR in LEAN
Language:Lean48 4 174
mlir-fuzz
A enumerator for MLIR, relying on the information given by IRDL.
Language:C++19 6 35
paper-template
A template for writing CS papers with latex -- includes CI, todonotes, ...
Language:TeX42 4 1014
Quidditch
IREE compiler and runtime for Snitch
Language:C++14 5 114
sail-riscv-lean
Language:Lean156
xdsl-smt
The implementation of an SMTLib dialect for xDSL
Language:Python16 6 36

opencompl's Repositories

opencompl/lean-mlir
A minimal development of SSA theory
Language:Lean197 4 12823
opencompl/paper-template
A template for writing CS papers with latex -- includes CI, todonotes, ...
Language:TeX42 4 1014
opencompl/mlir-fuzz
A enumerator for MLIR, relying on the information given by IRDL.
Language:C++19 6 35
opencompl/xdsl-smt
The implementation of an SMTLib dialect for xDSL
Language:Python16 6 36
opencompl/sail-riscv-lean
Language:Lean156
opencompl/Quidditch
IREE compiler and runtime for Snitch
Language:C++14 5 114
opencompl/riscv-lean
Language:Lean8
opencompl/fp-lean
Floating Point Semantics Mechanization for Lean
Language:Lean6 1 0
opencompl/riscv-paper-experiments
Language:MLIR52
opencompl/circomvent
A mechanization of the CIRCOM circuit semantics library
Language:Lean31
opencompl/sail-arm-lean
Language:Lean3
opencompl/DC-semantics-simulation-evaluation
In this repository we simulate the semantics of the DC dialect with verilator and (1) compare it against the semantics we mechanize with Lean-MLIR (2) assess the verification efforts at Handshake vs. DC level.
Language:C++1
opencompl/lean4
Lean 4 programming language and theorem prover
Language:Lean1 0 0
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.
Language:LLVM1 1 04
opencompl/attention-variants
Expressing attention as perfectly nested loops allows us to cultivate a wide variety of attention variants
Language:TeX
opencompl/bv-theorem-table-maker
Build the Bitvector table in the Lean bitvectors paper by looking up Lean's Environment
Language:Lean
opencompl/circt
Circuit IR Compilers and Tools
Language:C++
opencompl/csl_particle_flows
A template for writing CS papers with latex -- includes CI, todonotes, ...
Language:TeX
opencompl/evaluation-width-indep-bv
Evalaution for parametric bitvector decision procedures
opencompl/iree
A retargetable MLIR-based machine learning compiler and runtime toolkit.
Language:C++0 0
opencompl/lazystack-isl
Language:C1 0
opencompl/Leanwuzla
Connecting Bitwuzla to LeanSAT
Language:Lean0 0
opencompl/riscv-semantics-table
Replay the `Environment` for a given Lean module, ensuring that all declarations are accepted by the kernel.
Language:Lean0 0
opencompl/sail
Sail architecture definition language
Language:Isabelle1 0
opencompl/sail-arm
Sail version of Arm ISA definition, currently for Armv9.3-A, and with the previous Sail Armv8.5-A model
opencompl/sail-riscv
Sail RISC-V model
Language:C
opencompl/sail-riscv-lean-executable
Language:Lean0 01
opencompl/sail-riscv-lean-matchbv
Language:Lean
opencompl/sail-riscv-lean-small
Language:Python
opencompl/update-no-cache-mwe
Language:Lean