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 .