The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, though, has a few problems: induction isn't derivable, it isn't possible to prove 0 != 1, and pattern matching on algebraic data structures take linear time. In order to solve those issues, practical languages such as Coq are based on the Calculus of Inductive Constructions instead, which add a layer of primitive datatypes on top of CoC. That, unfortunately, makes the core language very complex.

An alternative solution to those problems is a new primitive, self, which is a construction that allows a type to reference its typed term. This construct, together with the Parigot encoding, and a slightly weakened but still useful notion of contradiction, is sufficient to solve the problems above. The proposed language, though, is still somewhat complex. In particular, it has different Pi types, complex kind machinery and requires a restricted form of recursion (for the Parigot encoding).

Is it possible to be simpler? I.e., can the calculus of constructions with only self types and nothing else from this paper still be able to derive induction and employ the parigot encoding?

| cite | improve this question | | | | |
  • $\begingroup$ This question would also be appropriate at CSTheory.stackexchange.com as it is about actively researched problems in logic, verification and programming languages. $\endgroup$ – Martin Berger Apr 28 '17 at 8:11
  • $\begingroup$ @MartinBerger you're correct. I have moved the question to this thread. I'll delete this post soon. If anyone is willing to reply, please do it there. $\endgroup$ – MaiaVictor Apr 28 '17 at 17:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.