# Difference between revisions of "Talk:Curry-Howard-Lambek correspondence"

From HaskellWiki

(Question on the origins of the terminology Curry-Howard-Lambek correspondence) |
(Signature) |
||

Line 3: | Line 3: | ||

:: Well, who cares. Curry-Howard is not descriptive enough for the special case of Haskell. Curry-Howard is very flexible. Works even for Pascal. Haskell seems more inclined to category theory these days, looks like the third part deserves more attention. --[[User:Uchchwhash|Pirated Dreams]] 06:04, 5 November 2006 (UTC) |
:: Well, who cares. Curry-Howard is not descriptive enough for the special case of Haskell. Curry-Howard is very flexible. Works even for Pascal. Haskell seems more inclined to category theory these days, looks like the third part deserves more attention. --[[User:Uchchwhash|Pirated Dreams]] 06:04, 5 November 2006 (UTC) |
||

::: Quite possibly, no one :). I was just giving my thoughts on why I hadn't renamed it, even though I had added the point about Lambek and CCC's. I'm happy to have it be "Curry-Howard-Lambek".[[User:BrettGiles|BrettGiles]] 21:03, 6 November 2006 (UTC) |
::: Quite possibly, no one :). I was just giving my thoughts on why I hadn't renamed it, even though I had added the point about Lambek and CCC's. I'm happy to have it be "Curry-Howard-Lambek".[[User:BrettGiles|BrettGiles]] 21:03, 6 November 2006 (UTC) |
||

− | : I'm interested in the history of the proof-as-program correspondence and I'm curious to see that the terminology Curry-Howard-Lambek correspondence is used in some contexts. Where does it come from? Is there a precise definition of it or a reference to it in the literature? I mean, Curry and Howard exhibited syntactic correspondences between Hilbert logic and typed combinatory logic on one side and between natural deduction and typed lambda-calculus on the other side but there is no such syntactic correspondence with CCCs. Is that correct? |
+ | : I'm interested in the history of the proof-as-program correspondence and I'm curious to see that the terminology Curry-Howard-Lambek correspondence is used in some contexts. Where does it come from? Is there a precise definition of it or a reference to it in the literature? I mean, Curry and Howard exhibited syntactic correspondences between Hilbert logic and typed combinatory logic on one side and between natural deduction and typed lambda-calculus on the other side but there is no such syntactic correspondence with CCCs. Is that correct? --[[User:Hugo Herbelin|Hugo Herbelin]] 16:10, 31 December 2007 (UTC) |

Types being "inhibited"? I thought they were "inhabited" by values, rather? I wouldn't know, so I'm not changing anything here. [[User:Isaac Dupree|Isaac Dupree]] 20:53, 17 November 2006 (UTC) |
Types being "inhibited"? I thought they were "inhabited" by values, rather? I wouldn't know, so I'm not changing anything here. [[User:Isaac Dupree|Isaac Dupree]] 20:53, 17 November 2006 (UTC) |

## Latest revision as of 16:10, 31 December 2007

Should this page be renamed Curry-Howard-Lambek correspondence? Makes a lot more sense that way. --Pirated Dreams 14:14, 4 November 2006 (UTC)

- Possibly. Personally, I didn't rename the page as it is seems to be more widely known just as "Curry-Howard" (e.g., wikipedia page is "Curry-Howard").BrettGiles 16:07, 4 November 2006 (UTC)
- Well, who cares. Curry-Howard is not descriptive enough for the special case of Haskell. Curry-Howard is very flexible. Works even for Pascal. Haskell seems more inclined to category theory these days, looks like the third part deserves more attention. --Pirated Dreams 06:04, 5 November 2006 (UTC)
- Quite possibly, no one :). I was just giving my thoughts on why I hadn't renamed it, even though I had added the point about Lambek and CCC's. I'm happy to have it be "Curry-Howard-Lambek".BrettGiles 21:03, 6 November 2006 (UTC)

- Well, who cares. Curry-Howard is not descriptive enough for the special case of Haskell. Curry-Howard is very flexible. Works even for Pascal. Haskell seems more inclined to category theory these days, looks like the third part deserves more attention. --Pirated Dreams 06:04, 5 November 2006 (UTC)
- I'm interested in the history of the proof-as-program correspondence and I'm curious to see that the terminology Curry-Howard-Lambek correspondence is used in some contexts. Where does it come from? Is there a precise definition of it or a reference to it in the literature? I mean, Curry and Howard exhibited syntactic correspondences between Hilbert logic and typed combinatory logic on one side and between natural deduction and typed lambda-calculus on the other side but there is no such syntactic correspondence with CCCs. Is that correct? --Hugo Herbelin 16:10, 31 December 2007 (UTC)

Types being "inhibited"? I thought they were "inhabited" by values, rather? I wouldn't know, so I'm not changing anything here. Isaac Dupree 20:53, 17 November 2006 (UTC)

- My mistake. Correcting. Thanks. --Pirated Dreams 13:47, 18 November 2006 (UTC)