|Authors||J. E. Hannay|
|Title||Abstraction Barrier-Observing Relational Parametricity|
|Afilliation||Software Engineering, Software Engineering|
|Publication Type||Proceedings, refereed|
|Year of Publication||2003|
|Conference Name||Typed Lambda Calculi and Applications. Proceedings of TLCA, 6th International Conference, Valencia, Spain, LNCS volume 2701|
|Date Published||June 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.