verified

Gems of verified things for educational purpose.

All known to compile under Coq 8.7.

Items

LTL: Linear temporal logic.
binary-heap: Binary heap.
binary-search-tree: Binary search tree.
binary-trie: Binary trie.
cps: Continuation passing style (CPS).
fast-power: Fast power method generalized to monoids.
finger-tree: Finger tree, specfied abstractly with a list.
group-theory: Group theory.
hoare: Hoare logic.
monads: Monad.
peterson: Peterson's locking algorithm.
sorting-algorithms: Various sorting algorithms including insert / selection / quick sort.
stlc-deptype: A STLC implementation with dependent type.
two-stack-queue: Queue implemented by two stacks with amotized O(1) complexity.
vect-deptype: Vector with dependent type.