Coq is a theorem prover that uses principles from type theory to provide formalizations of programs.

Libraries a neat representation of recursive and impure Coq programs function definitions for Coq metaprogramming

References index of coq tactics and their meanings coq and math? proving the biggest number in coq constructively

August 1, 2020