A concept of relational parametricity is developed taking into account the encapsulation mechanism inherent in universal types. This is then applied to 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. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Hannay, J. (2003). Abstraction barrier-observing relational parametricity. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2701, 135–152. https://doi.org/10.1007/3-540-44904-3_10
Mendeley helps you to discover research relevant for your work.