2022 Developer Survey is open! Take survey.

# Questions tagged [curry-howard]

The tag has no usage guidance.

9 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
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-...
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 ...
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 ...
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 ...
1 vote
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 ...
1 vote
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 ...
1 vote
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 ...