# Weakest model of computation that can typecheck?

What's the weakest (known) model of computation (or smallest language class) that can decide whether a simply-typed lambda calculus program type checks? What about an (explicitly typed) CoC program?

• Type checking for the simply typed $\lambda$-calculus is super easy. It's definitely primitive recursive, and probably much less. Calculus of constructions is a dependent type theory whose type checking involves equality checking, so that's going to be a lot more complicated, but I am not sure how to gauge that, precisely. Apr 25 '20 at 6:38
• The title of your question does not fit the actual question in the text. (Type checking STLC and CoC does not require the full power of Turing machines.) What are you really asking? Apr 25 '20 at 6:59