coq은(는) 여기로 연결됩니다.
로그라이크 오픈월드 게임에 대한 내용은 Caves of Qud 문서 참고하십시오.1. 개요
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로 개명하는 제안이 받아들여졌으며, 현재 추진 중이다.[2]
2. 외부 링크
[1] 프랑스어로 coq은 발음이 명확히 다르기 때문에 프랑스어 화자 입장에서는 억울할 수 있는 부분이다. Coq은 프랑스의 국립 연구소인 Inria에서 개발 했기 때문에 프랑스인의 기여가 큰 편이다.[2] Change of name: Coq -> The Rocq Prover