Equivalence in System F goes beyond beta-eta equivalence, due to parametric polymorphism. Syntactic logical relations and applicative bisimulations have been used as tools for reasoning about program equivalence in polymorphic languages. Nevertheless, even in the simplest case of pure System F, the connection between certain syntactic logical relations and program equivalence is not clear.

This talk is a call for discussion: We will focus on such questions; we will present alternative ways of stating them, and propose possible directions for answering them.