foreverbell / verified Public

Notifications You must be signed in to change notification settings
Fork 3
Star 44

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

44 stars 3 forks Branches Tags Activity

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 66 Commits
binary-heap		binary-heap
binary-search-tree		binary-search-tree
binary-trie		binary-trie
cps		cps
fast-power		fast-power
finger-tree		finger-tree
group-theory		group-theory
hoare		hoare
ltl		ltl
monads		monads
peterson		peterson
sorting-algorithms		sorting-algorithms
stlc-deptype		stlc-deptype
tactics @ bbe1bdc		tactics @ bbe1bdc
two-stack-queue		two-stack-queue
vect-deptype		vect-deptype
.gitignore		.gitignore
.gitmodules		.gitmodules
Makefile		Makefile
README.md		README.md

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.

coq formal-verification

Report repository

Releases

No releases published

Packages

Languages