On Proving Limited Completeness
Peter D. Mosses, Gordon D. Plotkin · DAIMI Report Series · 1985
We give 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.