In this talk, we present a trace model for System F that captures Strachey
parametric polymorphism. The model is built using operational nominal game
semantics and enforces parametricity by using names.
This model is used here to prove a conjecture of Abadi, Cardelli, Curien and
Plotkin which states that Strachey equivalence implies Reynolds equivalence
(i.e. relational parametricity) in System F.