Kripke logical relations and PCF (Q1898483)

\textit{A. Jung} and \textit{J. Tiuryn} [Lect. Notes Comput. Sci. 664, 245-257 (1993; Zbl 0795.03021)] introduced ``Kripke logical relations'' to characterize \(\lambda\)-definability. Here, these relations are used to show that \textit{K. Sieber's} model of PCF [``New steps toward full abstraction for local variables'', in: ACM SIGLPLAN Workshop on State in Programming Languages, 88-100 (1993)], consisting of continuous functions that are invariant under certain (finitary) logical relations, is fully abstract at all types.