Calculus of Constructions : 문서 추가

Author: damhiya

src/wiki/Calculus of Constructions.md

@@ -0,0 +1,10 @@
+---
+title: Calculus of Constructions
+categories: ["타입 이론"]
+license: CC BY-SA 4.0
+---
+
+Calculus of Constructions (CoC)는 [타입 이론](타입 이론)의 한가지이다. [Coq](Coq) 등의 [증명보조기](증명보조기)의 기반이론으로 이용된다. Impredicative \(\mathrm{Prop}\) [유니버스](타입 유니버스)를 가지고 있다는 점에서 [마틴뢰프 타입 이론](마틴뢰프 타입 이론)과 구분된다.
+
+## Calculus of Inductive Constructions (CIC)
+귀납적 타입을 추가한 CoC의 변종이다.

src/wiki/Coq.md

@@ -5,6 +5,7 @@ license: CC BY-SA 4.0
 ---
 
 Coq는 의존 타입 함수형 프로그래밍 언어이자 증명보조기이다.
+[Calculus of Inductive Constructions](Calculus of Constructions)에 기반하고 있다.
 
 ## 교재