Coq 입문

<Interactive Theorem Proving and Program Development>라는 책을 추천받아 조금씩 읽어보기로 했다. 첫 장에서는 Coq에 대한 간단한 안내를 진행한다. 책의 순서를 따라가면서 하나씩 알아보자 타입 먼저 Coq에서는 Gallina라는 언어를 사용해 요구사항(Specification)을 서술한다. 대부분의 다른 프로그래밍 언어들과 마찬가지로 타입은 declaration과 typing rule에 의해 정해진다.