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.
This work has been done with the support of EPSRC grant GR/M56333 and a British Council grant.
This author would like to acknowledge the support of an EPSRC Advanced Fellowship, EPSRC grant GR/L54639, and ESPRIT Working Group 6811 Applied Semantics
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alimohamed, A.: A Characterisation of Lambda Definability in Categorical Models of Implicit Polymorphism. Theoretical Computer Science 146 (1995) 5–23.
Fiore, M., Plotkin, G.D.: An axiomatisation of computationally adequate domain-theoretic models of FPC. Proc LICS 94. IEEE Press (1994) 92–102.
Hermida, C.A.: Fibrations, Logical Predicates and Indeterminates. Ph.D. thesis. Edinburgh (1993) available as ECS-LFCS-93-277.
Honsell, F., Sannella, D.T.: Pre-logical relations. Proc. CSL 99. LNCS 1683. Flum and Rodriguez-Artalejo (eds). Springer (1999) 546–562.
Jung, A., Tiuryn, J.: A new characterisation of lambda definability. Proc.TLCA. LNCS 664. Bezem and Groote (eds.) Springer (1993) 245–257.
Kinoshita, Y., O’Hearn, P., Power, A.J., Takeyama, M., Tennent, R.D.: An Axiomatic Approach to Binary Logical Relations with Applications to Data Refinement. Proc TACS 97. LNCS 1281. Abadi and Ito (eds). Springer (1997) 191–212.
Lambek, J., Scott, P.J.: Introduction to higher order categorical logic. Cambridge studies in advanced mathematics. Cambridge University Press (1986)
Ma, Q., Reynolds, J.C.: Types, abstraction and parametric polymorphism 2. Math. Found. of Prog. Lang. Sem. Lecture Notes in Computer Science. Springer (1991).
Mitchell, J.: Type systems for programming languages. Handbook of Theoretical Computer Science em B. van Leeuwen (ed). North-Holland (1990) 365–458.
Mitchell, J.: Foundations for programming languages. Foundations of Computing Series. MIT Press (1996).
Moggi, E.: Computational Lambda-calculus and Monads. Proc LICS 89 IEEE Press (1989) 14–23.
Plotkin, G.D., power, A.J., Sannella, D.T., Tennent, R.D.: Lax logical relations. (to appear in ICALP 2000).
Reynolds, J.C.: Types, abstraction, and parametric polymorphism. Information Processing 83 Mason (ed) North Holland (1983) 513–523.
Tennent, R.D.: Correctness of data representations in ALGOL-like languages. In: A Classical Mind, Essays in Honour of C.A.R. Hoare, A.W. Roscoe (ed.) Prentice-Hall (1994) 405–417.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Power, J., Robinson, E. (2000). Logical Relations and Data Abstraction. In: Clote, P.G., Schwichtenberg, H. (eds) Computer Science Logic. CSL 2000. Lecture Notes in Computer Science, vol 1862. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44622-2_34
Download citation
DOI: https://doi.org/10.1007/3-540-44622-2_34
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67895-3
Online ISBN: 978-3-540-44622-4
eBook Packages: Springer Book Archive