• 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
_CoqProject 347 Bytes