Skip to content
@opencompl

opencompl

README.md

Compiler Research at The University of Cambridge

This organization contains our research projects, collaborative research projects, as well as software that we develop for our community.

For further information, check out our website at https://grosser.science/.

Pinned Loading

  1. lean-mlir lean-mlir Public

    A minimal development of SSA theory

    Lean 265 29

  2. sail-riscv-lean sail-riscv-lean Public

    Lean 38 9

  3. paper-template paper-template Public

    A template for writing CS papers with latex -- includes CI, todonotes, ...

    TeX 46 21

Repositories

Showing 10 of 97 repositories
  • llvm-riscv-backend-evaluation Public

    Evaluating the performance of Veir's verified backend against LLVM.

    opencompl/llvm-riscv-backend-evaluation's past year of commit activity
    C 2 1 0 4 Updated Oct 1, 2026
  • veir Public

    Verified Intermediate Representation

    opencompl/veir's past year of commit activity
    Lean 114 34 42 (1 issue needs help) 43 Updated Oct 1, 2026
  • valaig Public

    Verified Model Checking Certificates in Lean

    opencompl/valaig's past year of commit activity
    Lean 3 1 0 0 Updated Oct 1, 2026
  • veir-sqlite Public
    opencompl/veir-sqlite's past year of commit activity
    MLIR 0 1 0 0 Updated Oct 1, 2026
  • veir-interpreter-scoreboard Public

    A scoreboard for `veir-interpret`

    opencompl/veir-interpreter-scoreboard's past year of commit activity
    LLVM 0 0 0 0 Updated Oct 1, 2026
  • sid-phd-thesis Public

    The one with my thesis

    opencompl/sid-phd-thesis's past year of commit activity
    TeX 2 0 0 0 Updated Sep 30, 2026
  • iree Public Forked from iree-org/iree

    A retargetable MLIR-based machine learning compiler and runtime toolkit.

    opencompl/iree's past year of commit activity
    C++ 0 Apache-2.0 1,045 0 0 Updated Sep 24, 2026
  • datapath-verification-paper Public Forked from opencompl/paper-template

    A template for writing CS papers with latex -- includes CI, todonotes, ...

    opencompl/datapath-verification-paper's past year of commit activity
    TeX 1 21 0 0 Updated Sep 21, 2026
  • paper-template Public

    A template for writing CS papers with latex -- includes CI, todonotes, ...

    opencompl/paper-template's past year of commit activity
    TeX 46 21 1 2 Updated Sep 16, 2026
  • llvm-project Public Forked from llvm/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/llvm-project's past year of commit activity
    LLVM 1 19,215 0 3 Updated Sep 14, 2026
View all repositories

Most used topics

lean4 floating-point