Skip to content

@weakmemory weakmemory

All

    Repositories list

    17 repositories

    • xmm

      Public
      Coq
      •1•0•0•1•Updated May 25, 2025May 25, 2025

    • promising2ToImm

      Public
      Promising 2.0 [Lee-al:PLDI20] to IMM compilation correctness proof
      Coq
      •
      MIT License
      •0•2•0•0•Updated Feb 10, 2025Feb 10, 2025

    • imm

      Public
      Intermediate Memory Model (IMM) and compilation correctness proofs for it
      coqproofweak-memory-models
      coqproofweak-memory-models
      Coq
      •
      MIT License
      •4•31•0•0•Updated Feb 5, 2025Feb 5, 2025

    • nixpkgs

      Public
      Nix Packages collection & NixOS
      Nix
      •
      MIT License
      •20k•0•0•0•Updated Aug 16, 2024Aug 16, 2024

    • hahnExt

      Public
      An extension to the Hahn library with extra definition and lemmas about sets and relations.
      Coq
      •0•0•0•0•Updated Jun 25, 2024Jun 25, 2024

    • local-coq-opam-archive

      Public
      Local archive for Coq related OPAM packages organized in various repositories
      0•0•0•0•Updated Jun 18, 2024Jun 18, 2024

    • hahn

      Public
      Hahn: A Coq library
      Coq
      •
      MIT License
      •15•0•0•0•Updated May 10, 2024May 10, 2024

    • promising-lib

      Public
      Coq
      •3•0•0•0•Updated Apr 16, 2024Apr 16, 2024

    • weakmemory.github.io

      Public
      0•0•0•0•Updated Feb 9, 2024Feb 9, 2024

    • promising-ir-coq

      Public
      Coq
      •1•0•0•0•Updated Oct 23, 2023Oct 23, 2023

    • sflib

      Public
      Coq
      •10•0•0•0•Updated Sep 25, 2023Sep 25, 2023

    • promising2-coq

      Public
      The Coq development of Promising 2.0 semantics for relaxed memory concurrency
      Coq
      •
      MIT License
      •1•0•0•0•Updated Jul 10, 2023Jul 10, 2023

    • weakestmoToImm

      Public
      The Weakestmo memory model and the compilation correctness proof to IMM
      Coq
      •
      MIT License
      •0•2•0•0•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
      •1•4•0•0•Updated Sep 7, 2022Sep 7, 2022

    • pwt

      Public
      A supplementary Coq formalization for "The Leaky Semicolon" paper
      Coq
      •
      MIT License
      •1•0•0•0•Updated Nov 11, 2021Nov 11, 2021

    • promising1ToImm

      Public
      Promising 1.0 [Kang-al:POPL17] to IMM compilation correctness proof
      Coq
      •
      MIT License
      •0•0•0•0•Updated May 13, 2020May 13, 2020

    • opam-ci

      Public
      Docker image containing OPAM for CI builds
      Dockerfile
      •3•0•0•0•Updated Apr 24, 2020Apr 24, 2020
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.