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....
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 ...
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 ...
Top 50 recent answers are included
Related Tags
type-theory × 531programming-languages × 118
dependent-types × 87
lambda-calculus × 71
type-checking × 64
type-inference × 51
functional-programming × 46
types-and-programming-languages × 46
logic × 38
category-theory × 28
reference-request × 26
terminology × 22
curry-howard × 21
inductive-datatypes × 20
polymorphisms × 20
homotopy-type-theory × 19
proof-assistants × 18
haskell × 18
coq × 16
typing × 16
compilers × 14
abstract-data-types × 12
notation × 11
computability × 10
induction × 10