[logicchains]

Since this seems to support inductive types, would it be correct to say that it's based on the calculus of inductive constructions (CIC), not the plain CoC? Basing a dependently-typed language on pure CoC (plus some other features weaker than inductive types; it's been proven impossible in CoC alone) is an open research problem (see e.g. Cedille and Formality).

[perthmad]

What do you mean? CoC definitely supports impredicative encodings, and as far as expressivity goes, this allows to implement a lot of programs. Proving them correct is another matter, but that's not what you implied. Also, CIC is notably not Turing-complete.

[logicchains]

I was referring to https://link.springer.com/chapter/10.1007/3-540-45413-6_16; induction is not derivable in pure CoC. I suppose yes technically you could base a dependently-typed language on it if you didn't mind not supporting induction, but I can't imagine many people wanting to use it, as it would be quite limited compared to one supporting inductive proofs. Or at least when people think of "dependently typed programming language", they're usually thinking of something at least as expressive as CIC.