# Questions tagged [curry-howard]

The tag has no usage guidance.

9 questions
Filter by
Sorted by
Tagged with
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 ...
599 views

### Simply typed lambda calculus and higher order logic

What is the relation between simply typed lambda calculus and higher order logic? Under Curry-Howard it seems that simply typed lambda calculus corresponds to propositional logic. How is it related ...
199 views

### Type-theoretic interpretation of Skolemization

What is the type-theoretic interpretation / equivalent of Skolemization? Skolemization converts some formula into Skolem normal form. The two formulae are equisatisfiable with each other. Or, to say ...
242 views

### How do continuations represent negations (under the Curry–Howard correspondence)?

Under the Curry–Howard correspondence, types can be thought of as propositions, and values inhabiting a type can be thought of as proofs that the corresponding proposition is true. (E.g., the ...
338 views

### Motivation for Dependent Type

By the Curry-Howard Isomorphism we view propositions (or theorems if true/inhabited) as types. But take the type $\mathbb{N} \implies \mathbb{N} \implies \mathbb{N}$. We have as witnesses to this ...
216 views

### Languages that lack contraction, weakening or exchange

When learning about generalized arrows, a question arised to me: Are there any languages (or potential languages) that lack one or more of the structural rules: contraction, weakeing and exchange? ...
158 views

### Can Curry-Howard prove a theorem from the types in your program, that has nothing to do with your program? [closed]

The following link states: Curry-Howard means that any type can be interpreted as a theorem in some logical system, and any term can be interpreted as a proof of its type. This does not mean that ...