Using methods drawn from Game Semantics, we build a sound and computationally adequate model of a simple calculus that includes
both subtyping and recursive types. Our model solves recursive type equations up to equality, and is shown to validate a subtyping
rule for recursive types proposed by Amadio and Cardelli.