A vary strangely named environment for interactive theorem proving
, somewhat like HOL
. COQ is French for rooster
From the COQ web page:
Developed in the LogiCal project, The Coq tool is a proof assistant which:
Coq is written in the Objective Caml language and uses the Camlp4 Pre-processor-pretty-printer for Objective Caml.
The current version of Coq is the 6.3.1. It is currently available for Unix and Windows 95/98/NT systems .