Logically Atomic Triples in Iris

Forked from FP / iris-atomic

  • Dan Frumin's avatar
    Add the ticket lock example · 892b1802
    Dan Frumin authored
    The specification for ticket lock is proven using the atomic
    specification for the increment operation.
    892b1802
Name
Last commit
Last update
build Loading commit data...
docs Loading commit data...
theories Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
Makefile Loading commit data...
Makefile.coq.local Loading commit data...
README.md Loading commit data...
_CoqProject Loading commit data...
awk.Makefile Loading commit data...
opam Loading commit data...