Coq

Coq는 의존 타입 함수형 프로그래밍 언어이자 증명보조기이다.

교재

Coq을 사용하는 프로그래밍 언어의 기초와 프로그램 검증에 대한 교재 시리즈 Software Foundations가 있다.