Talk:Calculus of constructions

From Wikipedia, the free encyclopedia

You have new messages (last change).

CoC can represent all functions provably total in higher-order logic, right? So, in what system is the strong normalization theory proved? Jim Apple 08:03, 19 August 2005 (UTC)

The inference rules presented in this article seem deficient. In particular, there is no way to prove anything of the form {\Gamma \vdash x : M N} from them. I imagine what's missing is a rule allowing one to derive x:A from a derivation of x:B and the beta-equality of A and B, or something like that. Hopefully, someone more familiar with this material can clear things up. -Chinju 17:41, 2 November 2005 (UTC)

Retrieved from "http://en.wikipedia.org../../../c/a/l/Talk%7ECalculus_of_constructions_24df.html"