Repositories list

• promising2ToImm

  Public
  Promising 2.0 [Lee-al:PLDI20] to IMM compilation correctness proof

  Coq

  •

  MIT License

  •00 forks in weakmemory/promising2ToImm•22 stars in weakmemory/promising2ToImm•00 issues in weakmemory/promising2ToImm•00 pull requests in weakmemory/promising2ToImm•Updated Oct 26, 2026Oct 26, 2026

• imm

  Public
  Intermediate Memory Model (IMM) and compilation correctness proofs for it

  coqproofweak-memory-models

  coqproofweak-memory-models

  Coq

  •

  MIT License

  •44 forks in weakmemory/imm•3232 stars in weakmemory/imm•00 issues in weakmemory/imm•00 pull requests in weakmemory/imm•Updated Oct 26, 2026Oct 26, 2026

• promising2-coq

  Public
  The Coq development of Promising 2.0 semantics for relaxed memory concurrency

  Coq

  •

  MIT License

  •11 fork in weakmemory/promising2-coq•00 stars in weakmemory/promising2-coq•00 issues in weakmemory/promising2-coq•00 pull requests in weakmemory/promising2-coq•Updated Oct 26, 2026Oct 26, 2026

• hahnExt

  Public
  An extension to the Hahn library with extra definition and lemmas about sets and relations.

  Coq

  •00 forks in weakmemory/hahnExt•00 stars in weakmemory/hahnExt•00 issues in weakmemory/hahnExt•00 pull requests in weakmemory/hahnExt•Updated Oct 26, 2026Oct 26, 2026

• hahn

  Public
  Hahn: A Coq library

  Coq

  •

  MIT License

  •1515 forks in weakmemory/hahn•00 stars in weakmemory/hahn•00 issues in weakmemory/hahn•00 pull requests in weakmemory/hahn•Updated Oct 26, 2026Oct 26, 2026

• xmm

  Public
  Coq

  •11 fork in weakmemory/xmm•00 stars in weakmemory/xmm•00 issues in weakmemory/xmm•11 pull request in weakmemory/xmm•Updated May 25, 2025May 25, 2025

• nixpkgs

  Public
  Nix Packages collection & NixOS

  Nix

  •

  MIT License

  •21k21k forks in weakmemory/nixpkgs•00 stars in weakmemory/nixpkgs•00 issues in weakmemory/nixpkgs•00 pull requests in weakmemory/nixpkgs•Updated Aug 16, 2024Aug 16, 2024

• local-coq-opam-archive

  Public
  Local archive for Coq related OPAM packages organized in various repositories

  00 forks in weakmemory/local-coq-opam-archive•00 stars in weakmemory/local-coq-opam-archive•00 issues in weakmemory/local-coq-opam-archive•00 pull requests in weakmemory/local-coq-opam-archive•Updated Jun 18, 2024Jun 18, 2024

• promising-lib

  Public
  Coq

  •33 forks in weakmemory/promising-lib•00 stars in weakmemory/promising-lib•00 issues in weakmemory/promising-lib•00 pull requests in weakmemory/promising-lib•Updated Apr 16, 2024Apr 16, 2024

• weakmemory.github.io

  Public
  00 forks in weakmemory/weakmemory.github.io•00 stars in weakmemory/weakmemory.github.io•00 issues in weakmemory/weakmemory.github.io•00 pull requests in weakmemory/weakmemory.github.io•Updated Feb 9, 2024Feb 9, 2024

• promising-ir-coq

  Public
  Coq

  •11 fork in weakmemory/promising-ir-coq•00 stars in weakmemory/promising-ir-coq•00 issues in weakmemory/promising-ir-coq•00 pull requests in weakmemory/promising-ir-coq•Updated Oct 23, 2023Oct 23, 2023

• sflib

  Public
  Coq

  •1010 forks in weakmemory/sflib•00 stars in weakmemory/sflib•00 issues in weakmemory/sflib•00 pull requests in weakmemory/sflib•Updated Sep 25, 2023Sep 25, 2023

• weakestmoToImm

  Public
  The Weakestmo memory model and the compilation correctness proof to IMM

  Coq

  •

  MIT License

  •00 forks in weakmemory/weakestmoToImm•22 stars in weakmemory/weakestmoToImm•00 issues in weakmemory/weakestmoToImm•00 pull requests in weakmemory/weakestmoToImm•Updated Sep 20, 2022Sep 20, 2022

• fairness

  Public
  This repository contains the supplementary Coq development for the Making Weak Memory Models Fair paper.

  Coq

  •

  MIT License

  •11 fork in weakmemory/fairness•44 stars in weakmemory/fairness•00 issues in weakmemory/fairness•00 pull requests in weakmemory/fairness•Updated Sep 7, 2022Sep 7, 2022

• pwt

  Public
  A supplementary Coq formalization for "The Leaky Semicolon" paper

  Coq

  •

  MIT License

  •11 fork in weakmemory/pwt•00 stars in weakmemory/pwt•00 issues in weakmemory/pwt•00 pull requests in weakmemory/pwt•Updated Nov 11, 2021Nov 11, 2021

• promising1ToImm

  Public
  Promising 1.0 [Kang-al:POPL17] to IMM compilation correctness proof

  Coq

  •

  MIT License

  •00 forks in weakmemory/promising1ToImm•00 stars in weakmemory/promising1ToImm•00 issues in weakmemory/promising1ToImm•00 pull requests in weakmemory/promising1ToImm•Updated May 13, 2020May 13, 2020

• opam-ci

  Public
  Docker image containing OPAM for CI builds

  Dockerfile

  •33 forks in weakmemory/opam-ci•00 stars in weakmemory/opam-ci•00 issues in weakmemory/opam-ci•00 pull requests in weakmemory/opam-ci•Updated Apr 24, 2020Apr 24, 2020