[TYPES] logical relations
eijiro.sumii at gmail.com
Thu Jan 26 00:11:01 EST 2006
Thank you very much for all the replies (both private and public).
Many of them have pointed out the lambda-definability papers by
Plotkin. I managed to get a copy of the one in Curry Festschrift
(thanks to my colleagues).
HOWEVER, according to my quick "eye grep" of this paper, it does not
seem to contain the words "logical relations" nor
"main/basic/fundamental lemma/theorem" anywhere, so I still do not
know the answer to the "for what reason" part of my question. Perhaps
I should try harder to get the 1973 tech report (as well as other
original papers by Tait and Statman).
By the way, there was also a similar question back in 1988 in Types
and a reply by Prof. John Mitchell
but even he does not seem to have known a clear answer...!
P.S. A few people asked me why I am asking. The primary reason is my
own curiosity, but this time my question was also inpired by a student
who loves to know.
More information about the Types-list