Logical Relations and Data Abstraction

John Power, Edmund Robinson

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

We prove, in the context of simple type theory, that logical relations are sound and complete for data abstraction as given by equational specifications. Specifically, we show that two implementations of an equationally specified abstract type are equivalent if and only if they are linked by a suitable logical relation. This allows us to introduce new types and operations of any order on those types, and to impose equations between terms of any order. Implementations are required to respect these equations up to a general form of contextual equivalence, and two implementations are equivalent if they produce the same contextual equivalence on terms of the enlarged language. Logical relations are introduced abstractly, soundness is almost automatic, but completeness is more difficult, achieved using a variant of Jung and Tiuryn’s logical relations of varying arity. The results are expressed and proved categorically.
Original languageEnglish
Title of host publicationComputer Science Logic: 14th InternationalWorkshop, CSL 2000 Annual Conference of the EACSL Fischbachau, Germany, August 21 – 26, 2000 Proceedings
Place of PublicationHeidelberg
PublisherSpringer
Pages497-511
Number of pages15
Volume1862
DOIs
Publication statusPublished - 2001

Fingerprint Dive into the research topics of 'Logical Relations and Data Abstraction'. Together they form a unique fingerprint.

  • Cite this

    Power, J., & Robinson, E. (2001). Logical Relations and Data Abstraction. In Computer Science Logic: 14th InternationalWorkshop, CSL 2000 Annual Conference of the EACSL Fischbachau, Germany, August 21 – 26, 2000 Proceedings (Vol. 1862, pp. 497-511). Springer. https://doi.org/10.1007/3-540-44622-2_34