[TYPES] logical relations

[Coquand]

 As a complement to the reference to Tait's 1967 article, one can add
the paper
(from notes of a course by Statman, 1985)

 R. Gandy
 On the axiom of extensionality, part I
 Journal of Symbolic Logic, 36-48, 1956

which gives an interpretion of extensional type theory in intensional
type theory using logical relations (the extensional equality being
defined for higher types by induction).

------------

 A similar question: who introduced first the term "computational
adequacy theorem" for Theorem 3.1 of the "LCF considered as a programming
language" paper??

               Thierry Coquand