14 May
2007
14 May
'07
4:26 a.m.
On 5/13/07, Josef Svenningsson
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