4

At a technical level, I understand the Curry-Howard correspondence in various settings, and its usefulness as a technical tool. What I'm looking for is a fairly rigorous discussion of genuinely philosophical consequences of the CH correspondence. So, for example, does the resulting 'propositions as types' slogan just mean that propositions can be represented as types, or that propositions really are types?

The literature is full of computer scientists making vague and not especially precise claims about the philosophical significance of the CH correspondence, but frankly I find most of these discussions very casual and sloppy. Is there a non-trivial, substantive philosophical claim about the nature of proofs or propositions that flows naturally from the CH correspondence? Even just references to good literature would be helpful.

provocateur
  • 139
  • 2
  • 3
    Does this answer your question? [Logic and Computation: a philosophical viewpoint on Curry-Howard isomorphism](https://philosophy.stackexchange.com/questions/42352/logic-and-computation-a-philosophical-viewpoint) – Conifold Oct 02 '20 at 20:12
  • I struggle to find anything substantive and rigorous in that discussion. – provocateur Oct 03 '20 at 15:15
  • Also related (as it turned out in a discussion on that as well) https://philosophy.stackexchange.com/questions/92607/what-is-the-relationship-between-algorithms-and-logic – Fizz Jul 30 '22 at 18:23

0 Answers0