AuthorsJ. E. Hannay
TitleAbstraction Barrier-Observing Relational Parametricity
AfilliationSoftware Engineering, Software Engineering
Publication TypeProceedings, refereed
Year of Publication2003
Conference NameTyped Lambda Calculi and Applications. Proceedings of TLCA, 6th International Conference, Valencia, Spain, LNCS volume 2701
Date PublishedJune 10 - 12

A concept of relational parametricity is developed where the encapsulation mechanism inherent in universal types is taken into account. This is then applied in the context of data types and refinement, naturally giving rise to a notion of simulation relations that compose for data types with higher-order operations, and whose existence coincides with observational equivalence. The ideas are developed syntactically in lambda calculus with a relational logic. The new notion of relational parametricity is asserted axiomatically, and a corresponding parametric PER-semantics is devised.

Citation KeySE.5.Hannay.2003.b