Questions tagged [curry-howard]
The curry-howard tag has no usage guidance.
9
questions with no upvoted or accepted answers
4
votes
0
answers
71
views
What is the role of abstract machines in the Curry-Howard isomorphism?
By abstract machines I mean things like the SECD machine, Krivine's machine or more generally machines with states/memory/registers/stack/accumulator...
According to Wikipedia page of the Curry-...
- 483
3
votes
0
answers
111
views
Understanding $\lambda \mu$-calculus in more programming way
I am learning $\lambda \mu$-calculus (self-study).
I learned it because it seems very useful for understanding Curry-Howard correspondence (e.g understanding the connection between classical logic ...
- 247
2
votes
0
answers
66
views
How can we derive this representation of existential types?
I know that an existential type $ \exists t. t $ can be represented using universally quantified types as $ \forall r. (\forall t. t \rightarrow r) \rightarrow r $ and I have some basic intuition for ...
2
votes
0
answers
165
views
Curry howard isomorphism "proof as program"
I'm reading CH Isomorphism.
Let's divide into two stages:
Prop corresponds to types. so a proposition A $\wedge$ B corresponds to type A $\times$ B.
Proof corresponds to the program. What is the ...
- 883
1
vote
0
answers
25
views
Analogue of disjunction and existence properties for a Turing-complete programming language?
Quoting from Wikipedia:
In mathematical logic, the disjunction and existence properties are
the "hallmarks" of constructive theories such as Heyting arithmetic
and constructive set theories ...
- 111
1
vote
0
answers
61
views
How do program types such as natural numbers figure into the Curry-Howard Isomorphism?
In Coq, the nat, the type of natural numbers, has type Set. By the Curry-Howard Isomorphism, all propositions of type ...
- 31
1
vote
0
answers
52
views
Curry howard Isomorphism what the propositions A , B ranges over
In CH-I what the propositions A , B ranges over too ?
An update :
From Pfennings notes :
"A denotes proposition about the mathematical objects such as integer or a real number."
From :
Per ...
- 883
0
votes
0
answers
37
views
Axiomatic Geometry expressed with algebraic data types & functions
I've been trying to express an axiomatic geometry [1] using a typed functional language (OCaml so far).
My motivation comes from [2] and the claim "Programs correspond to logical proofs".
In ...
- 1
0
votes
0
answers
37
views
How do you derive a type $∃e(e)$ in terms of universally quantified types, without invoking Void initially?
I wrote a "proof" for this, and though it was enough to convince myself, there are a few things that bother me about it. Primarily I'm not sure about the loose way in which I'm swapping between first-...
- 153