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
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-...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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-...
user avatar
  • 153