A Trace Semantics for System F Parametric Polymorphism
Guilhem Jaber, Nikos Tzevelekos · Lecture notes in computer science · 2018
We present a trace model for Strachey parametric polymorphism. The model is built using operational nominal game semantics and captures parametricity by using names. It is used here to prove an operational version of a conjecture of Abadi, Cardelli, Curien and Plotkin which states that Strachey equivalence implies Reynolds equivalence in System F. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.