I put a related question on Computer Science Stack Exchange a week ago. Linking it here in the hopes that HN users roll-calling here will shed some light.
I'm surprised Andrej didn't give a longer answer. He usually does. In a type theory the type system and calculus are the same thing, not really two things glued together (although there are some of those.) Those used for theorem proving and programming (CIC, MLTT, etc) aren't Turing complete by themselves. Different type theories do differ in computational strength. How is this possible? Well think about it, if you couldn't express the type of the Y combinator then you couldn't use it. Schemes like recursion, induction-recursion and induction-induction allow more power to be added to the language.
To answer you more directly, one starts with the most powerful system, the lambda calculus and then one restricts its power using types. Finding the goldilocks zone of the right amount of power is one of the primary things type theory research has been about. Type theories vary in decidability, those that aren't decidable aren't usually used for theorem provers or as substrata for programming languages.
To answer you more directly, one starts with the most powerful system, the lambda calculus and then one restricts its power using types. Finding the goldilocks zone of the right amount of power is one of the primary things type theory research has been about. Type theories vary in decidability, those that aren't decidable aren't usually used for theorem provers or as substrata for programming languages.