Authors | J. E. Hannay |
Title | Axiomatic Criteria for Quotients and Subobjects at Higher Order |
Afilliation | Software Engineering, Software Engineering |
Status | Published |
Publication Type | Proceedings, refereed |
Year of Publication | 2003 |
Conference Name | Automata, Languages and Programming. Proceedings of ICALP 2003, 30th International Colloquium, Eindhoven, the Netherlands, LNCS volume 2719 |
Pagination | 903-917 |
Date Published | June 30 - July 4 |
Publisher | Springer-Verlag |
Abstract | 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. 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. |
Citation Key | SE.5.Hannay.2003.a |