The second-order lambda calculus allows an elegant formalisation of
abstract data types (ADT's) using existential types.
Plotkin and Abadi's logic for parametricity  [PA93]
then provides the useful proof principle of *simulation*
for ADT's,
which can be used to show equivalence of data representations.
However, we show that this logic is not sufficient for reasoning
about specifications of ADT's,
and we present an extension of the logic that does provide 
the proof principles for ADT's that we want.

[PA93]
Gordon Plotkin and Martin Abadi.
A logic for parametric polymorphism.
In TLCA'93, volume 664 of Lecture Notes in Computer Science,
pages 361--375, 1993.