New answers tagged type-theory
1
vote
Curry-Howard isomorphism and non-constructive logic
The Curry-Howard correspondence is not crucial for functioning of a proof assistant. Unforunately, the term "Curry-Howard correspondence" seems to be misused nowadays for all sorts of things....
- 29.9k
3
votes
Curry-Howard isomorphism and non-constructive logic
While proof assistants typically use constructive mathematics, the Curry-Howard-Correspondence does not necessarily require constructivism.
The important aspect of the correspondence is that the ...
- 131
7
votes
Curry-Howard isomorphism and non-constructive logic
I think people sometimes disagree on what exactly Curry-Howard is. But, one way to look at it is an exact correspondence between the syntactic rules for logic and for type theory.
For the ...
- 2,579
Top 50 recent answers are included