snu-sf / promising-coq
The Coq development of A Promising Semantics for Relaxed-Memory Concurrency
☆33Updated last month
Related projects ⓘ
Alternatives and complementary repositories for promising-coq
- Formally verified implementation of Alive in Lean☆35Updated last year
- We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation …☆49Updated 6 months ago
- Problem Sets for MIT 6.887 Formal Reasoning About Programs, Spring 2017☆20Updated 7 years ago
- Cerberus C semantics☆53Updated this week
- Lenses in Coq☆16Updated 2 years ago
- ☆51Updated this week
- Deadlock freedom by type checking☆19Updated last year
- Bedrock Bit Vector Library☆27Updated 8 months ago
- An implementation of the Chord lookup protocol verified in Coq using the Verdi framework☆10Updated 5 years ago
- A Coq library for parametric coinduction☆43Updated last month
- Coq library for tactics, basic definitions, sets, maps☆42Updated last week
- Coq library on rewriting theory and termination☆35Updated 3 weeks ago
- Intermediate Memory Model (IMM) and compilation correctness proofs for it☆21Updated 3 months ago
- An enhanced unification algorithm for Coq☆49Updated this week
- Finite sets and maps for Coq with extensional equality☆29Updated last year
- A formalization of properties of a simple imperative, memory-safe language.☆19Updated 3 years ago
- Hoare Type Theory☆69Updated last month
- LVC verified compiler☆57Updated 6 years ago
- ☆11Updated last month
- A Seamless, Interactive Tactic Learner and Prover for Coq☆59Updated last week
- Implementation of Nuprl's type theory in Coq☆44Updated 3 years ago
- ☆22Updated 8 years ago
- Coq library for verified low-level programming☆57Updated 7 years ago
- Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq☆95Updated 3 months ago
- Coq formalizations and proofs of (data) structures and algorithms.☆46Updated 6 years ago
- Best of POPL (BOP) Reading Group Memoirs☆67Updated 2 years ago
- A Gallina compiler with C++17 as an intermediate representation☆42Updated 3 years ago
- A mechanisation of Wasm in Coq☆97Updated 2 weeks ago
- Easy SMT solver interaction☆24Updated this week
- A type checker for the Lean theorem prover☆39Updated 3 years ago