Definition: Coq

An open source language used to develop and prove mathematical formulas. Introduced in 1989, the name Coq is a play on words from Thierry Coquand, one of the developers, and Calculus of Constructions (CoC). Coq means "rooster" in French, and its specification language is "Gallina," which is "hen" in Spanish.