There are several good reasons to call it Coq: - The person who implemented the first version (?) is called Coquand. - The french have a tradition of naming t

There are several good reasons to call it Coq: - The person who implemented the first version (?) is called Coquand. - The french have a tradition of naming their software projects after animals. - Coq is french for Rooster. But to be honest, there is a rather persistent tale that Thierry Coquand's advisor, Gérard Huet, did it on purpose to offend his American colleagues who were too "politically correct" for his tastes. He also named a certain programming language "Caml". This does have a perfect innocuous explanation, but also happens to be the name of a certain cigarette brand. This was in 1985, when smoking started to be banned in many public places...