AuthorsJ. E. Hannay
TitleAxiomatic Criteria for Quotients and Subobjects at Higher Order
AfilliationSoftware Engineering, Software Engineering
StatusPublished
Publication TypeProceedings, refereed
Year of Publication2003
Conference NameAutomata, Languages and Programming. Proceedings of ICALP 2003, 30th International Colloquium, Eindhoven, the Netherlands, LNCS volume 2719
Pagination903-917
Date PublishedJune 30 - July 4
PublisherSpringer-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 KeySE.5.Hannay.2003.a