What is the origin of logical relations? I actually have two questions:


Who first used logical relations to relate semantics?

I traced them back to Reynold's "On the Relation Between Direct and Continuation Semantics", but I can't claim to have made an exhaustive search.

I have found references to logical relations dating earlier (Tait, '67), but not for relating semantics. 
What is the best current introduction for logical relations? 


I know of Mitchell's "Type Systems for Programming Languages" from the Handbook of TCS. What other expositions are there?
Plotkin used logical relations in his unpublished but nevertheless widely circulated and influential 1973 paper "Lambda Definability and Logical Relations". I have a copy of this note on my webpage.

I used to think that this is where the name came from, but when I asked Rick Statman about this, he told me that Mike Gordon coined the term logical relation to describe Tait's method, and that he and Gordon Plotkin picked it up from him. I think this is how it entered programming language jargon, though you could make sure by asking Plotkin.