<p>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?</p>

CC BY-SA 4.0
2020-04-25T06:38:02.180Z
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.
Andrej Bauer
CC BY-SA 4.0
2020-04-25T06:59:40.580Z
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?
Andrej Bauer
<automata-theory><type-theory>
Weakest model of computation that can typecheck?
bitconfused
# Weakest model of computation that can typecheck?

(Asked by: username_0 on 2020-04-24)

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?

**Tags:** automata-theory, type-theory

> **Comments:**
> **username_1**: 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.  
> **username_1**: 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?  

---

## 0 answers

