Skip to main content
Theoretical Computer Science

Return to Question

Tweeted twitter.com/#!/StackCSTheory/status/42862526769270784
added 82 characters in body; edited tags
Source Link
Hsien-Chih Chang 張顯之
Hsien-Chih Chang 張顯之
  • 7.7k
  • 4
  • 45
  • 83

Given that the Curry-Howard CorrespondenceCurry-Howard Correspondence is so widely spread/extended, is there any difference between proofs and programs (or between propositions and types)? Can we really identify them?

Given that the Curry-Howard Correspondence is so widely spread/extended, is there any difference between proofs and programs (or between propositions and types)? Can we really identify them?

Given that the Curry-Howard Correspondence is so widely spread/extended, is there any difference between proofs and programs (or between propositions and types)? Can we really identify them?

Post Migrated Here from stackoverflow.com (revisions)
Source Link
plmday
plmday

What is the difference between proofs and programs (or between propositions and types)?

Given that the Curry-Howard Correspondence is so widely spread/extended, is there any difference between proofs and programs (or between propositions and types)? Can we really identify them?