Cursed curry howard
October 19, 2022 —
sameer
Table of Contents
Decidability
why it matters?
Because your program can have more bits than there are atoms in universe.
Function types in haskell for inststance aren't decidable, with due exceptions. Analogy
| Logic | TT | Haskell |
| P | A | a |
| P/\Q | A*B | (a,b) |
| P->Q | A->B | either(a,b) |
| ∀ x P(x) | ∏ a: a P(a) | |
| ∃ x P(a) | ∑ a: a P(a) | |
| proof | inhabitant | program |
table reference
Papers
intuitionistic games : determinacy , completeness and normalization
automata theory approach to inutionistic logic
objects of interest
Axiom K
constructive
intutionistic
Induction
bar induction
l¨ob induction 🏿
Created: 2022-10-30 Sun 10:06