A logic for abstract data types as existential types

Abstract

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 sucient for reasoning about specications of ADT’s, and we present an extension of the logic that does provide the proof principles for ADT’s that we want.