|
|
|
|
|
|
by samth
3319 days ago
|
|
|
Extraction of terms written using Fixpoint isn't really the Curry-Howard correspondence. Instead, the correspondence is between (for example) proofs of correctness and terms in the Calculus of Constructions. [Fixpoint terms are also CIC programs, so there's a sense in which they're related, but it's not really about Curry-Howard.] |
|
|