[TYPES] logical relations

Coquand coquand at cs.chalmers.se
Thu Jan 26 09:50:33 EST 2006

 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

More information about the Types-list mailing list