Skip to content

@opencompl opencompl

Change the repository type filter

All

    Repositories list

    74 repositories

    • sail-riscv-lean

      Public
      Lean
      •3•7•0•4•Updated Aug 10, 2025Aug 10, 2025

    • lean-mlir

      Public
      A minimal development of SSA theory
      Lean
      •
      Other
      •20•156•39•20•Updated Aug 8, 2025Aug 8, 2025

    • paper-blockten

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

    • iree

      Public
      A retargetable MLIR-based machine learning compiler and runtime toolkit.
      C++
      •
      Apache License 2.0
      •742•0•0•0•Updated Aug 8, 2025Aug 8, 2025

    • lean4

      Public
      Lean 4 programming language and theorem prover
      Lean
      •
      Apache License 2.0
      •639•0•0•10•Updated Aug 7, 2025Aug 7, 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
      •8•0•0•0•Updated Aug 7, 2025Aug 7, 2025

    • xdsl-smt

      Public
      The implementation of an SMTLib dialect for xDSL
      Python
      •5•15•2•2•Updated Aug 5, 2025Aug 5, 2025

    • paper-hydra-in-lean

      Public
      The one where we re-implement Hydra in Lean
      TeX
      •17•0•0•0•Updated Aug 4, 2025Aug 4, 2025

    • sail

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

    • csl_particle_flows

      Public
      A template for writing CS papers with latex -- includes CI, todonotes, ...
      TeX
      •17•0•0•0•Updated Jul 30, 2025Jul 30, 2025

    • paper-bv-multi-width-parametric-solver

      Public
      The paper on parametric multi-width solvers
      TeX
      •17•1•0•0•Updated Jul 27, 2025Jul 27, 2025

    • paper-template

      Public
      A template for writing CS papers with latex -- includes CI, todonotes, ...
      computer-sciencetemplatelatexpaperwriting
      TeX
      •17•41•0•0•Updated Jul 27, 2025Jul 27, 2025

    • riscv-paper-experiments

      Public
      MLIR
      •1•4•15•6•Updated Jul 24, 2025Jul 24, 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 Jul 23, 2025Jul 23, 2025

    • Quidditch

      Public
      IREE compiler and runtime for Snitch
      C++
      •
      Apache License 2.0
      •4•12•9•7•Updated Jul 17, 2025Jul 17, 2025

    • paper-verification-llvm-backend

      Public template
      A template for writing CS papers with latex -- includes CI, todonotes, ...
      TeX
      •17•0•0•0•Updated Jul 15, 2025Jul 15, 2025

    • mlir-fuzz

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

    • evaluation-width-indep-bv

      Public
      Evalaution for parametric bitvector decision procedures
      0•0•0•0•Updated Jul 3, 2025Jul 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
      •8•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-arm-lean

      Public
      Lean
      •0•3•0•0•Updated Jun 8, 2025Jun 8, 2025

    • sail-riscv

      Public
      Sail RISC-V model
      C
      •
      Other
      •223•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