Skip to content

Coq formalizations and proofs of (data) structures and algorithms.

Notifications You must be signed in to change notification settings

foreverbell/verified

Repository files navigation

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.

About

Coq formalizations and proofs of (data) structures and algorithms.

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published