|
|
|
|
|
|
by carnitine
1802 days ago
|
|
|
Curry-Howard isn’t that specific, nor do dependent types correspond to first-order logic. Curry-Howard is a broad correspondence between logics and type theories. System F, which is weaker than dependent type theory corresponds to higher-order logic. First-order logic actually doesn’t actually correspond to a popular type system, though the correspondence of course exists. |
|
|