Coq 프로그래밍 언어 함수형 프로그래밍 언어 증명 보조기 Coq는 의존 타입 함수형 프로그래밍 언어이자 증명보조기이다. 교재 Coq을 사용하는 프로그래밍 언어의 기초와 프로그램 검증에 대한 교재 시리즈 Software Foundations가 있다. 외부 링크 공식 웹사이트