PCF, Kripke logic relations, logic relations
Sieber has described a model of PCF consisting of continuous functions that are invariant under certain (finitary) logical relations, and shown that it is fully abstract for closed terms of up to third-order types. We show that one may achieve full abstraction at all types using a form of "Kripke logical relations" introduced by Jung and Tiuryn to characterize λ definability.
O'Hearn, Peter W. and Riecke, John G., "Kripke Logical Relations and PCF" (1995). L.C. Smith College of Engineering and Computer Science - Former Departments, Centers, Institutes and Projects. Paper 3.