COQ - Everything2.com

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:

allows to handle calculus assertions,
to check mechanically proofs of these assertions,
helps to find formal proofs,
extracts a certified program from the constructive proof of its formal specification.

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 .

HoL	NuPRL	French slang	Why Do You Hate Ra
Natural Deduction	Type Theory	Curry-Howard Isomorphism	Objective Caml
Caml	200	Rooster	Cor
Coo	Conditional Proof	figure skating	theorem
Q	Windows	Unix