Coq is an interactive theorem prover first released in 1989. It allows for the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification.
- website
- A released pdf or current refl can be found in document page.
- PNP
- Lecture notes for a short course on proving/programming in Coq via SSReflect.
- Math Comp
- math-comp
- hs-to-coq
- Convert Haskell source code to Coq source code.