Full abstraction by translation

This paper shows how a fully abstract model for a rich metalanguage such as FPC can be used to prove theorems about other languages. In particular. we use results obtained from a game semantics of FPC to show that the natural translation of the lazy lambda-calculus into the metalanguage is fully abstract, thus obtaining a new full abstraction result from an old one. The proofs involved are very easy-all the hard work was done in giving the original games model. So far we have been unable to prove the completeness of our translation without recourse to the denotational model; we therefore have an indication of the worth of such fully abstract models.