The
Coq proof assistant is a
formal proof management system that is based on the Curry-Howard
(
propositions-as-types,
formulas-as-types,
proofs-as-programs) correspondence.
Coq au vin (literally,
“cock in wine”) analyzes some aspects of this correspondence
(propositional logic, predicate logic, and proof irrelevance) and
provides some examples of “proofs viewed as programs.” In
addition, it compares Coq with the
Agda proof
assistant through the Curry-Howard correspondence.