Talk:Curry-Howard-Lambek correspondence

From HaskellWiki
Jump to navigation Jump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

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)
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)