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.