calculus of constructions

이 개념이 constructive proof에 대응되는 타입 체계로서 고안된 점을 고려하여 “증명짓기 계산법”을 재안합니다.

값과 타입 구분없이 자유롭게 계산의 대상이고 결과가 될 수 있는 계산세계이므로.