Coq is an interactive theorem prover based on the Calculus of Inductive Constructions.

Coq is an interactive theorem prover based on the calculus of inductive constructions.

Resources