Kripke Logical Relations and PCF
Peter W. O’Hearn, Jon G. Riecke · Information and Computation · 1995
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.