Coq

Coq는 1989년에 처음 출시된 증명 보조기(대화형 정리 증명기)이다. 유형 이론의 일종인 구성 계산(Calculus of constructions)을 이론적 기초로 한다. INRIA의 티에리 코캉(Thierry Coquand) 등 프랑스 과학자들이 주도적으로 개발하였다. 2025년 출시된 버전에서 Rocq로 개칭되었다.

같이 보기