[Haskell-cafe] Higher order types via the Curry-Howard correspondence

[Gaal Yahas]

On 5/13/07, Josef Svenningsson <josef.svenningsson at gmail.com> wrote:
> I think both Benja's and David's answers are terrific. Let me just add
> a reference.

Yes, this entire thread has been quite illuminating. Thanks all!

> The person who's given these issues most thought is probably Per
> Martin-Löf. [...]
> In the beginning of the third lecture you will find the classic quote:
> "the meaning of a proposition is determined by what it is to verify
> it, or what counts as a verification of it"

I like how this is reminiscent of Quine's ideas in "On What There Is".

Another reference to add is Simon Thompson, _Type Theory and
Functional Programming_,
which I stumbled upon online here:
http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ .

-- 
Gaal Yahas <gaal at forum2.org>
http://gaal.livejournal.com/