1. 개요
https://coq.inria.fr/Coq는 CIC(Calculus of Inductive Constructions)에 기반한 증명보조기이다. OCaml과 마찬가지로 프랑스의 Inria에서 개발되었다. 구현은 OCaml로 되어있으며, Coq 코드를 OCaml이나 Haskell로 추출하여 프로그래밍 언어로도 사용할 수 있다.
Coq이라는 단어는 프랑스어로 수탉이라는 뜻이 있으며, 동시에 Coq의 기반 이론인 CoC(Calculus of Constructions)와 CoC의 개발자중 한명인 Thierry Coquand 등을 중의적으로 의미한다. 한편 Coq과 영어권 은어 'cock'의 발음 유사성 때문에[1] Coq을 Rocq로 개명하는 제안이 받아들여졌으며, 현재 추진중에 있다. Change of name: Coq -> The Rocq Prover
[1]
프랑스어로 coq은 발음이 명확히 다르기 때문에 프랑스어 화자 입장에서는 억울할 수 있는 부분이다. Coq은 프랑스의 국립 연구소인 Inria에서 개발 했기 때문에 프랑스인의 기여가 큰 편이다.