New answers tagged

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....
Andrej Bauer's user avatar
  • 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 ...
NaCl's user avatar
  • 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 ...
Dan Doel's user avatar
  • 2,579

Top 50 recent answers are included