On Proving Limiting Completeness
Peter D. Mosses, Gordon D. Plotkin · SIAM Journal on Computing · 1987
We give two proofs of Wadsworth’s classic approximation theorem for the pure $\lambda $-calculus. One of these illustrates a new method utilising a certain kind of intermediate semantics for proving correspondences between denotational and operational semantics. The other illustrates a direct technique of Milne, employing recursively-specified inclusive relations.