Questions tagged [curry-howard]
The curry-howard tag has no usage guidance.
16
questions
4
votes
1
answer
142
views
Connection between strong normalization of the simply typed λ-calculus, and cut elimination for propositional logic
What is the precise connection between:
strong normalization of the simply typed $\lambda$-calculus, and
cut elimination for (intuitionistic) propositional logic (limited to implication) in “sequent ...
- 619
1
vote
0
answers
67
views
Do game semantics for logic have Curry-Howard-like correspondence with game semantics for programming languages?
Both for logic and PLs do have notion of game semantics. Both are defined by two-player dialogue game, but players are different. In first case it is game between Verifyer and Falsifyer and in second ...
- 295
0
votes
0
answers
66
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
1
vote
0
answers
149
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
740
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 ...
- 377
9
votes
2
answers
758
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
194
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
104
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 ...
- 109
8
votes
1
answer
319
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
9
votes
2
answers
750
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 ...
- 193
1
vote
0
answers
85
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 ...
- 51
3
votes
2
answers
291
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,571
3
votes
2
answers
480
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 ...
- 51
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 ...
- 461
14
votes
1
answer
894
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
175
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,581