Abstract
We introduce an axiomatic approach to logical relations and data refinement. We consider a programming language and the monad on the category of small categories generated by it. We identify abstract data types for the language with sketches for the associated monad, and define an axiomatic notion of “relation” between models of such a sketch in a semantic category. We then prove three results: (i) such models lift to the whole language together with the sketch; (ii) any such relation satisfies a soundness condition, and (iii) such relations compose. We do this for both equality of data representations and for an ordered version. Finally, we compare our formulation of data refinement with that of Hoare.
This work has been done with the support of the MITI Cooperative Architecture Project. This author also acknowledges the support of Kaken-hi.
This author acknowledges the support of the MITI Cooperative Architecture Project.
This author acknowledges the support of EPSRC grant GR/J84205, Frameworks for programming languages and logics, and the MITI Cooperative Architecture Project.
This author acknowledges the support of an operating grant from the Natural Sciences and Engineering Research Council of Canada.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Michael Barr and Charles Wells. Toposes, Triples and Theories, volume 278 of Grundlagen der mathentatischen Wissenschaften. Springer-Verlag, 1985.
D. Gries, editor. Programming Methodology, A Collection of Articles by IFIP WG 2.3. Springer-Verlag, New York, 1978.
Claudio A. Hermida. Fibrations, Logical Predicates, and Indeterminates. PhD thesis, The University of Edinburgh, 1993. Published as CST-103-93, also as ECS-LFCS-93-277.
C.A.R. Hoare. Data refinement in a categorical setting. Unpublished manuscript, 1987.
C.A.R. Hoare and He Jifeng. Data refinement in a categorical setting. Oxford Computing Laboratory Technical Monograph PRG-90, 1990.
G.M. Kelly and A.J. Power. Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads. Journal of Pure and Applied Algebra, 89:163–179, 1993.
Y. Kinoshita and A.J. Power. Data refinement and algebraic structure. ETL Technical Report TR96-2, Electrotechnical Laboratory, January 1996.
Y. Kinoshita and A.J. Power. Lax naturality through enrichment. Journal of Pure and Applied Algebra, 112(1):53–72, 1996.
Yoshiki Kinoshita, A. John Power, and Makoto Takeyama. Sketches. Submitted, 1996.
QingMing Ma and J. C. Reynolds. Types, abstraction, and parametric polymorphism, part 2. In S. Brookes et al., editors, Mathematical Foundations of Programming Semantics, Proceedings of the 7th International Conference, volume 598 of Lecture Notes in Computer Science, pages 1–40. Springer-Verlag, Berlin, 1992, Pittsburgh, PA, March 1991.
J. C. Mitchell. Representation independence and data abstraction. pages 263–276.
J.C. Mitchell and A. Scedrov. Notes on sconing and relators. In E. Boerger et al., editors, Computer Science Logic: 6th Workshop, CSL '92: Selected Papers, volume 702 of Lecture Notes in Computer Science, pages 352–378, San Miniato, Italy, 1992. Springer-Verlag, Berlin.
P. W. O'Hearn and R. D. Tennent. Parametricity and local variables. J. ACM, 42(3):658–709, May 1995. Also in [14].
P.W. O'Hearn and R.D. Tennent, editors. Algol-like Languages, volume 2. Birkhauser, Boston, 1997.
A. M. Pitts. Relational properties of domains. Information and Computation, 127:66–90, 1996.
G. Plotkin and M. Abadi. A logic for parametric polymorphism. In M. Bezen and J. F. Groote, editors, Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 361–375, Utrecht, The Netherlands, March 1993. Springer-Verlag, Berlin.
G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223–255, 1977.
A. J. Power. Premonoidal categories as categories with algebraic structure. Submitted.
J. C. Reynolds. User-defined types and procedural data structures as complementary approaches to data abstraction. In S. A. Schuman, editor, New Advances in Algorithmic Languages 1975, pages 157–168. Inst. de Reserche d'Informatique et d'Automatique, Rocquencourt, France, 1975. Reprinted in [2], pages 309–317.
J. C. Reynolds. Types, abstraction and parametric polymorphism. In R. E. A. Mason, editor, Information. Processing 83, pages 513–523. North Holland, Amsterdam, 1983.
E. P. Robinson. Logical relations and data abstraction. Extended abstract.
E. P. Robinson and G. Rosolim. Reflexive graphs and parametric polymorphism. In Proceedings, 9th Annual IEEE Symposium on Logic in Computer Science, Paris, 1994. IEEE Computer Society Press, Los Alamitos, California.
D. S. Scott. A type-theoretical alternative to CUCH, ISWIM, OWHY. Privately circulated memo, Oxford University, October 1969. Published in Theoretical Computer Science, 121(1/2):411–440, 1993.
H. Thielecke. Continuation passing style and self adjointness. Continuations Workshop, Paris, January, 1997.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kinoshita, Y., O'Hearnt, P.W., Power, A.J., Takeyama, M., Tennent, R.D. (1997). An axiomatic approach to binary logical relations with applications to data refinement. In: Abadi, M., Ito, T. (eds) Theoretical Aspects of Computer Software. TACS 1997. Lecture Notes in Computer Science, vol 1281. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014552
Download citation
DOI: https://doi.org/10.1007/BFb0014552
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63388-4
Online ISBN: 978-3-540-69530-1
eBook Packages: Springer Book Archive