Games and Full Abstraction for a Functional Metalanguage with Recursive Types

In particular, fully abstract models have been found for various kinds of languages with local variables [8,13-16], and a fully complete games model of the polymorphic language System F has been constructed by Hughes [59].