Skip to content

@opencompl opencompl

Change the repository type filter

All

    Repositories list

    72 repositories

    • lean-mlir

      Public
      A minimal development of SSA theory
      MLIR
      •
      Other
      •20•185•43•31•Updated Oct 7, 2025Oct 7, 2025

    • sail-riscv-lean

      Public
      Lean
      •5•11•1•4•Updated Oct 7, 2025Oct 7, 2025

    • mlir-fuzz

      Public
      A enumerator for MLIR, relying on the information given by IRDL.
      C++
      •5•19•1•1•Updated Oct 7, 2025Oct 7, 2025

    • sail-arm-lean

      Public
      Lean
      •0•3•0•0•Updated Oct 7, 2025Oct 7, 2025

    • Quidditch

      Public
      IREE compiler and runtime for Snitch
      C++
      •
      Apache License 2.0
      •4•13•9•8•Updated Oct 6, 2025Oct 6, 2025

    • xdsl-smt

      Public
      The implementation of an SMTLib dialect for xDSL
      Python
      •4•16•2•1•Updated Oct 3, 2025Oct 3, 2025

    • paper-template

      Public
      A template for writing CS papers with latex -- includes CI, todonotes, ...
      computer-sciencetemplatelatexpaperwriting
      TeX
      •13•42•1•1•Updated Oct 1, 2025Oct 1, 2025

    • riscv-paper-experiments

      Public
      MLIR
      •1•4•15•4•Updated Sep 26, 2025Sep 26, 2025

    • lean4

      Public
      Lean 4 programming language and theorem prover
      Lean
      •
      Apache License 2.0
      •674•0•0•9•Updated Sep 26, 2025Sep 26, 2025

    • iree

      Public
      A retargetable MLIR-based machine learning compiler and runtime toolkit.
      C++
      •
      Apache License 2.0
      •769•0•0•0•Updated Sep 26, 2025Sep 26, 2025

    • evaluation-width-indep-bv

      Public
      Evalaution for parametric bitvector decision procedures
      0•0•0•0•Updated Sep 16, 2025Sep 16, 2025

    • DC-semantics-simulation-evaluation

      Public
      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.
      C++
      •0•1•0•0•Updated Sep 16, 2025Sep 16, 2025

    • circomvent

      Public
      A mechanization of the CIRCOM circuit semantics library
      Lean
      •1•3•0•0•Updated Sep 11, 2025Sep 11, 2025

    • llvm-project

      Public
      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.
      LLVM
      •
      Other
      •15k•1•0•3•Updated Sep 11, 2025Sep 11, 2025

    • csl_particle_flows

      Public
      A template for writing CS papers with latex -- includes CI, todonotes, ...
      TeX
      •13•0•0•0•Updated Aug 25, 2025Aug 25, 2025

    • circt

      Public
      Circuit IR Compilers and Tools
      C++
      •
      Other
      •374•0•0•0•Updated Aug 14, 2025Aug 14, 2025

    • riscv-semantics-table

      Public
      Replay the `Environment` for a given Lean module, ensuring that all declarations are accepted by the kernel.
      Lean
      •
      Apache License 2.0
      •9•0•0•0•Updated Aug 11, 2025Aug 11, 2025

    • sail

      Public
      Sail architecture definition language
      Isabelle
      •
      Other
      •140•0•0•2•Updated Aug 3, 2025Aug 3, 2025

    • update-no-cache-mwe

      Public
      Lean
      •0•0•0•0•Updated Jul 2, 2025Jul 2, 2025

    • fp-lean

      Public
      Floating Point Semantics Mechanization for Lean
      leanfloating-pointlean4
      Lean
      •
      Apache License 2.0
      •0•5•0•0•Updated Jun 30, 2025Jun 30, 2025

    • bv-theorem-table-maker

      Public
      Build the Bitvector table in the Lean bitvectors paper by looking up Lean's Environment
      Lean
      •
      Apache License 2.0
      •9•0•0•0•Updated Jun 30, 2025Jun 30, 2025

    • sail-riscv-lean-executable

      Public
      Lean
      •1•0•0•0•Updated Jun 27, 2025Jun 27, 2025

    • Leanwuzla

      Public
      Connecting Bitwuzla to LeanSAT
      Lean
      •6•0•0•0•Updated Jun 19, 2025Jun 19, 2025

    • sail-riscv

      Public
      Sail RISC-V model
      C
      •
      Other
      •231•0•0•2•Updated Jun 1, 2025Jun 1, 2025

    • sail-riscv-lean-matchbv

      Public
      Lean
      •0•0•0•0•Updated May 30, 2025May 30, 2025

    • sail-arm

      Public
      Sail version of Arm ISA definition, currently for Armv9.3-A, and with the previous Sail Armv8.5-A model
      Isabelle
      •
      Other
      •23•0•0•0•Updated May 26, 2025May 26, 2025

    • attention-variants

      Public
      Expressing attention as perfectly nested loops allows us to cultivate a wide variety of attention variants
      TeX
      •0•0•0•0•Updated Apr 25, 2025Apr 25, 2025

    • lazystack-isl

      Public
      C
      •
      MIT License
      •0•0•0•0•Updated Feb 28, 2025Feb 28, 2025

    • lazystack-barvinok

      Public
      Barvinok modified for lazystack
      C
      •
      GNU General Public License v2.0
      •0•0•0•0•Updated Feb 26, 2025Feb 26, 2025

    • lazystack-polylib

      Public
      Polylib modified for Lazystack
      C
      •
      MIT License
      •0•0•0•0•Updated Feb 26, 2025Feb 26, 2025