Skip to main content
SpringerLink
Log in
Book cover

International Conference on Mathematics of Program Construction

MPC 2002: Mathematics of Program Construction pp 23–39Cite as

Logical Relations and Galois Connections

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2386))

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Samson Abramsky. Abstract interpretation, logical relations, and Kan extensions. J. Logic and Computation, 1(1):5–41, 1990.

    Article  MATH  MathSciNet  Google Scholar 

  2. 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.

    Google Scholar 

  3. 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.

    Google Scholar 

  4. Peter J. de Bruin. Inductive Types in Constructive Languages. PhD thesis, Rijksuniversiteit Groningen, 1995.

    Google Scholar 

  5. 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.

  6. 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.

    Google Scholar 

  7. 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.

    Google Scholar 

  8. 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.

    Google Scholar 

  9. Paul Hoogendijk. A Generic Theory of Datatypes. PhD thesis, Department of Mathematics and Computing Science, Eindhoven University of Technology, 1997.

    Google Scholar 

  10. J. Hartmanis and R.E. Stearns. Pair algebras and their application to automata theory. Information and Control, 7(4):485–507, 1964.

    Article  MathSciNet  Google Scholar 

  11. J. Hartmanis and R.E. Stearns. Algebraic Structure Theory of Sequential Machines. Prentice-Hall, 1966.

    Google Scholar 

  12. Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of Program Analysis. Springer-Verlag, 1998.

    Google Scholar 

  13. 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.

    Google Scholar 

  14. J.C. Reynolds. Types, abstraction and parametric polymorphism. In R.E. Mason, editor, IFIP’83, pages 513–523. Elsevier Science Publishers, 1983.

    Google Scholar 

  15. P. Wadler. Theorems for free! In 4’th Symposium on Functional Programming Languages and Computer Architecture, ACM, London, September 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computing Laboratory, University of Oxford, Oxford, OX1 3QD, England

    Kevin Backhouse

  2. School of Computer Science and Information Technology, University of Nottingham, Nottingham, NG8 1BB, England

    Roland Backhouse

Authors
  1. Kevin Backhouse
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Roland Backhouse
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computing Laboratory, University of Kent at Canterbury, CT2 7NF, Canterbury, Kent, UK

    Eerke A. Boiten

  2. Institut für Informatik, Universität Augsburg, Universitätsstr. 14, 86135, Augsburg, Germany

    Bernhard Möller

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation