Abstract
Algebraic properties of logical relations on partially ordered sets are studied. It is shown how to construct a logical relation that extends a collection of base Galois connections to a Galois connection of arbitrary higher-order type. “Theorems-for-free” is used to show that the construction ensures safe abstract interpretation of parametrically polymorphic functions.
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
Samson Abramsky. Abstract interpretation, logical relations, and Kan extensions. J. Logic and Computation, 1(1):5–41, 1990.
K.S. Backhouse. A functional semantics of attribute grammars. In International Conference on Tools and Algorithms for Construction and Analysis of Systems, Lecture Notes in Computer Science. Springer-Verlag, 2002. Available from: http://web.comlab.ox.ac.uk/oucl/research/areas/progtools/publications.htm.
R.C. Backhouse, P. de Bruin, P. Hoogendijk, G. Malcolm, T.S. Voermans, and J. van der Woude. Polynomial relators. In M. Nivat, C.S. Rattray, T. Rus, and G. Scollo, editors, Proceedings of the 2nd Conference on Algebraic Methodology and Software Technology, AMAST’91, pages 303–326. Springer-Verlag, Workshops in Computing, 1992.
Peter J. de Bruin. Inductive Types in Constructive Languages. PhD thesis, Rijksuniversiteit Groningen, 1995.
R.C. Backhouse, T.S. Voermans, and J. van der Woude. A relational theory of datatypes. Available via World-Wide Web at http://www.cs.nott.ac.uk/~rcb/MPC/papers. Available via anonymous ftp from ftp://ftp.win.tue.nl in directory pub/math.prog.construction, December 1992.
Patrick Cousot and Radhia Cousot. Abstract interpretation: A unifed lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM Symposium on Principles of Programming Languages, pages 238–252, Los Angeles, California, January 1977.
Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. In Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, pages 269–282, San Antonio, Texas, January 1979.
Patrick Cousot and Radhia Cousot. Higher-order abstract interpretations (and application to comportment analysis generalizing strictness, termination, projection and per analysis of functional languages). In Procs. ICCL’94, IEEE, pages 95–112, 1994.
Paul Hoogendijk. A Generic Theory of Datatypes. PhD thesis, Department of Mathematics and Computing Science, Eindhoven University of Technology, 1997.
J. Hartmanis and R.E. Stearns. Pair algebras and their application to automata theory. Information and Control, 7(4):485–507, 1964.
J. Hartmanis and R.E. Stearns. Algebraic Structure Theory of Sequential Machines. Prentice-Hall, 1966.
Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of Program Analysis. Springer-Verlag, 1998.
Gordon D. Plotkin. Lambda-definability in the full type hierarchy. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, London, 1980.
J.C. Reynolds. Types, abstraction and parametric polymorphism. In R.E. Mason, editor, IFIP’83, pages 513–523. Elsevier Science Publishers, 1983.
P. Wadler. Theorems for free! In 4’th Symposium on Functional Programming Languages and Computer Architecture, ACM, London, September 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Backhouse, K., Backhouse, R. (2002). Logical Relations and Galois Connections. In: Boiten, E.A., Möller, B. (eds) Mathematics of Program Construction. MPC 2002. Lecture Notes in Computer Science, vol 2386. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45442-X_4
Download citation
DOI: https://doi.org/10.1007/3-540-45442-X_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43857-1
Online ISBN: 978-3-540-45442-7
eBook Packages: Springer Book Archive