Questions tagged [curry-howard]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
20
votes
2answers
1k views

Is there a typed lambda calculus which is consistent and Turing complete?

Is there a typed lambda calculus where the corresponding logic under the Curry-Howard correspondence is consistent, and where there are typeable lambda expressions for every computable function? This ...