We’re rewarding the question askers & reputations are being recalculated! Read more.

Questions tagged [typed-lambda-calculus]

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 ...
21
votes
2answers
3k views

How do you get the Calculus of Constructions from the other points in the Lambda Cube?

The CoC is said to be the culmination of all three dimensions of the Lambda Cube. This isn't apparent to me at all. I think I understand the individual dimensions, and the combination of any two seems ...
4
votes
1answer
220 views

What is a term of the type $\bot\rightarrow A$?

The sentence $\bot\rightarrow A$ is provable in intuitionistic logic for any type $A$. The proof is trivial: \begin{align} \bot&\vdash\bot \\ \hline \bot&\vdash A \\ \hline &\vdash\bot\...
2
votes
0answers
154 views

Heyting algebra in simply typed lambda calculus

The Emil Jeřábek's comment in Can boolean algebra be expressed in simply typed lambda caclulus? give rise to the following question: Can some non-trivial Heyting algebra be expressed in simply typed ...