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?

  • 4
    $\begingroup$ 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. $\endgroup$ Apr 25 '20 at 6:38
  • 1
    $\begingroup$ 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? $\endgroup$ Apr 25 '20 at 6:59

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.