Axiomatic criteria are given for the existence of higher-order maps over subobjects and quotients. These criteria are applied in showing the soundness of a method for proving specification refinement up to observational equivalence. This generalises the method to handle data types with higher-order operations, using standard simulation relations. We also give a direct setoid-based model satisfying the criteria. The setting is the second-order polymorphic lambda calculus and the assumption of relational parametricity. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Hannay, J. (2003). Axiomatic criteria for quotients and subobjects for higher-order data types. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2719, 903–917. https://doi.org/10.1007/3-540-45061-0_70
Mendeley helps you to discover research relevant for your work.