Quoting Wikipedia "Many systems of type theory, such as the simply-typed lambda calculus, intuitionistic type theory, and the calculus of constructions, are also programming languages." I'm a Coq user and, to some extent, familiar with CoC. How CoC differs from intuitionistic type theory (Martin-Löf type theory?) and what are the major consequences of it? Both for proving theorems and for programming.

  • $\begingroup$ This seems to be very similar to the following question on cstheory. $\endgroup$
    – cody
    Commented Apr 28, 2015 at 20:30


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.