| open import Data.Unit | |
| open import Data.Empty | |
| open import Data.Product | |
| open import Data.Bool using (Bool; true; false; not; _∧_; _∨_) | |
| open import Data.Nat | |
| open import Data.Nat.Properties | |
| open import Data.Nat.Induction | |
| open import Data.Fin using (Fin) | |
| open import Relation.Binary.PropositionalEquality | |
| open import Induction.WellFounded |
(Borrowing terminology from https://unison-lang.org/, which is what prompted me to think about / write this.)
Scroll down to "Examples" to see how this would be used in practice.
The representation of abilities uses mutable references, a primitive that can be expressed naturally in interaction combinators. Here, they're implemented
| // SPDX-License-Identifier: MIT | |
| // Copyright 2024 Higher Order Company | |
| //! An 'atomic fuzzer' to exhaustively test an atomic algorithm for correctness. | |
| //! | |
| //! This fuzzer can test an algorithm with every possible ordering of parallel | |
| //! instructions / update propagation. | |
| //! | |
| //! This module implements a subset of the [`std::sync::atomic`] api. To test an | |
| //! algorithm with the fuzzer, it must first be compiled to use this module's |