Questions tagged [curry-howard]
The curry-howard tag has no usage guidance.
4
questions
16
votes
2
answers
1k
views
Does the Y combinator contradict the Curry-Howard correspondence?
The Y combinator has the type $(a \rightarrow a) \rightarrow a$. By the Curry-Howard Correspondence, because the type $(a \rightarrow a) \rightarrow a$ is inhabited, it must correspond to a true ...
- 263
2
votes
2
answers
580
views
Is Wadler's 'Theorems for Free' as general as Design By Contract for establishing correctness?
Philip Wadler has written a brilliant paper called 'Theorems for Free'. The big idea is that you can use types to reason about your program, and even prove simple theorems about your program.
We see ...
- 1,189
7
votes
1
answer
526
views
Curry Howard correspondence to Predicate Logic?
So I'm trying to get my head round Curry-Howard. (I've tried at it several times, it's just not gelling/seems too abstract). To tackle something concrete, I'm working through the couple of Haskell ...
- 477
6
votes
1
answer
465
views
Non-termination of types in Martin-Löf's Type:Type?
In the pre-history of dependent type theory, Per Martin Löf
introduced a calculus that is in some sense the simplest dependent
type theory and the most general form of impredicative polymorphism.
It ...
- 8,178