Coq
- 프로그래밍 언어
- 함수형 프로그래밍 언어
- 증명 보조기
Coq는 의존 타입 함수형 프로그래밍 언어이자 증명보조기이다. Calculus of Inductive Constructions에 기반하고 있다.
교재
Software Foundations
SF 시리즈는 소프트웨어의 수학적 기초에 대한 교재로, 모든 내용이 Coq으로 형식화 되어있다. 현재 총 6권으로 구성되어있다.
Certified Programming with Dependent Types
CPDT는 Coq와 소프트웨어 검증 등을 다루는 교재이다. SF 시리즈에 비해 난이도가 비교적 높다.
Coq'Art
Coq'Art는 Coq와 Calculus of Inductive Constructions에 대한 교재이다. 프랑스어판은 무료 pdf를 제공하고 있으나, 영어판은 일부 챕터만 무료로 공개돼있다.