Relational Parametricity for Higher Kinds
I just gave a talk at CSL 2012 on "Relational Parametricity for Higher Kinds". In the paper I explain how to extend the usual relationally parametric models of polymorphic types to handle higher kinded types, like the ones found in Haskell and Scala. As a consequence, you get encodings of things like equality types, higher-kinded existential types and higher-kinded initial algebras, with nice reasoning principles.
The slides:
The paper, with abstract, is available here.