Created: 2023-04-21 07:47
Reference Wikipedia
The Curry-Howard correspondence is a generalization of a syntactic analogy between systems of formal logic and computational calculi. It was first discovered by the American mathematician Haskell Curry and the logician William Alvin Howard
This link between logic and computation is usually attributed to Curry and Howard, although the idea is related to the operational interpretation of intuitionistic logic given in various previous formulations.
It is based on the observation that two families of seemingly unrelated formalisms—namely, the proof systems on one hand, and the models of computation on the other—are in fact the same kind of mathematical objects.