# Questions tagged [curry-howard]

The tag has no usage guidance.

14 questions
Filter by
Sorted by
Tagged with
0 votes
0 answers
54 views

### How can we establish that Gödel's completeness theorem corresponds to an interactive disassembler?

I have came across an idea from Jean-Louis Krivine, in this article written in French (page 7 to 10), where he dresses up an equivalence between an operating system and an axiomatic system: A utility ...
1 vote
0 answers
128 views

### What is the model of computation that corresponds (in the manner of Curry-Howard) to the deduction rule of resolution?

The Curry-Howard Correspondence is well-documented for the isomorphism which associates the intuitionistic natural deduction proof calculus (logic side) with the type system for the simply typed ...
• 81
8 votes
3 answers
682 views

### What's the logical counterpart to jumps with arguments on CPS terms?

It's well known that the CPS (continuation-passing style) translation often employed in compilers corresponds to double negation translation under the Curry-Howard isomorphism. Though often the target ...
• 293
9 votes
2 answers
449 views

### Why is the Curry-Howard isomorphism?

The Curry-Howard isomorphism is the correspondence between type systems (like for the simply typed lambda calculus) and proof systems (like natural deduction). More precisely, types resemble ...
• 101
4 votes
0 answers
182 views

### What logic do refinement types correspond to?

I'm interested in applicability of refinement types to theorem-proving hence the questions about their logical expressiveness. Let's say, we have a type system which corresponds to some logic ...
• 41
0 votes
0 answers
99 views

### Curry Howard Isomorphism and cut elimination

I am currently reading about the proof for the isomorphism between Gentzen's sequent calculus $G$ and the simply typed lambda calculus $\lambda(\rightarrow,\times)$. The proof assumes the cut-free ...
8 votes
1 answer
291 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 ...
• 181
7 votes
2 answers
634 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 ...
• 173
1 vote
0 answers
84 views

### Equality Theorems with Type Theoretic Proof

I am investigating how I might be able to translate even commonplace equalities/ inequalities via the so-called Curry-Howard Correspondance - from a generic, set theoretic plus AOC foundation - into a ...
3 votes
2 answers
275 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? ...
• 2,501
3 votes
2 answers
437 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 ...
20 votes
2 answers
2k 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 ...
14 votes
1 answer
835 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 ...
• 195
3 votes
2 answers
169 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 ...
• 2,541