Skip to main content
SpringerLink
Log in
Book cover

Algol-like Languages pp 165–185Cite as

Birkhäuser

Reasoning About Local Variables with Operationally-Based Logical Relations

  • Chapter

Part of the book series: Progress in Theoretical Computer Science ((PTCS))

Abstract

A parametric logical relation between the phrases of an Algol-like language is presented. Its definition involves the structural operational semantics of the language, but was inspired by denotationally-based work of O’Heam and Reynolds on translating Algol into a predicatively polymorphic linear lambda calculus. The logical relation yields an applicative characterisation of contextual equivalence for the language and provides a useful (and complete) method for proving equivalences. Its utility is illustrated by giving simple and direct proofs of some contextual equivalences, including an interesting equivalence due to O’Hearn which hinges upon the undefinability of ‘snapback’ operations (and which goes beyond the standard suite of ‘Meyer-Sieber’ examples). Whilst some of the mathematical intricacies of denotational semantics are avoided, the hard work in this operational approach lies in establishing the ‘fundamental property’ for the logical relation—the proof of which makes use of a compactness property of fixpoint recursion with respect to evaluation of phrases. But once this property has been established, the logical relation provides a verification method with an attractively low mathematical overhead.

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   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   109.99
Price excludes VAT (USA)
  • Durable hardcover 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. F. Honsell, I. A. Mason, S. F. Smith, and C. L. Talcott. A variable typed logic of effects. Information and Computation, 119 (1): 55–90, May 1995.

    Article  MathSciNet  MATH  Google Scholar 

  2. D. J. Howe. Equality in lazy computation systems. In 4th Annual Symposium on Logic in Computer Science, pages 198–203. IEFF Computer Society Press, Washington, 1989.

    Google Scholar 

  3. D. J. Howe. Proving congruence of bisimulation in functional programming languages. Information and Computation, 124 (2): 103–112, February 1996.

    Article  MathSciNet  MATH  Google Scholar 

  4. R. Milner. Fully abstract models of typed lambda-calculi. Theoretical Computer Science, 4: 1–22, 1977.

    Article  MathSciNet  MATH  Google Scholar 

  5. J. C. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B, pages 365458. North-Holland, Amsterdam, 1990.

    Google Scholar 

  6. A. Meyer and K. Sieber. Towards fully abstract semantics for local variables. In Proc. 15th Symp. on Principles of Programming Languages, San Diego,pages 191–203. ACM, 1988. See Chapter 7.

    Google Scholar 

  7. I. A. Mason, S. F. Smith, and C. L. Talcott. From operational semantics to domain theory. Information and Computation (to appear). Revised and extended version of [Smi92].

    Google Scholar 

  8. F. J. 01es. Types algebras, functor categories and block structure. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, chapter 15, pages 543–574. Cambridge University Press, 1985. See Chapter 11.

    Google Scholar 

  9. P. W. O’Heam and U. S. Reddy. Objects, Interference and the Yoneda Embedding. In S. Brookes, M. Main, A. Melton, and M. Mislove, editors, Mathematical Foundations of Programming Semantics, Eleventh Annual Conference,volume 1 of Electronic Notes in Theoretical Computer Science,Tulane University, New Orleans, Louisiana, March 29-April 1 1995. Elsevier Science.

    Google Scholar 

  10. P. W. O’Hearn and J. C. Reynolds. From ALGOL to polymorphic linear lambda calculus. Lectures at the Isaac Newton Institute for Mathematical Sciences, Cambridge UK, August 1995.

    Google Scholar 

  11. P. W. O’Hearn and R. D. Tennent. Parametricity and local variables. Journalof the ACM,42(3):658–709, 1995. See Chapter 16.

    Google Scholar 

  12. A. M. Pitts. Relational properties of domains. Information and Computation, 1996. To appear. A preliminary version appeared as Cambridge Univ. Computer Laboratory Technical Report Number 321, December, 1993.

    Google Scholar 

  13. A. M. Pitts. Operationallybased theories of program equivalence. In P. Dybjer and A. M. Pitts, editors, Semantics and Logics of Computation. Cambridge University Press (to appear).

    Google Scholar 

  14. A. M. Pitts and I. D. B. Stark. Operational reasoning for functions with local state. In A. D. Gordon and A. M. Pitts, editors, Higher Order Operational Techniques in Semantics. In preparation.

    Google Scholar 

  15. A. M. Pitts and I. D. B. Stark. Observable properties of higher order functions that dynamically create local names, or: What’s new? In Mathematical Foundations of Computer Science, Proc. 18th Int. Symp., Gdansk, 1993, volume 711 of Lecture Notes in Computer Science, pages 122–141. Springer-Verlag, Berlin, 1993.

    Chapter  Google Scholar 

  16. U. S. Reddy. Global state considered unnecessary: Introduction to objectbased semantics. Lisp and Symbolic Computation,9(1):7–76, 1996. See Chapter 19.

    Google Scholar 

  17. J. C. Reynolds. The essence of ALGOL. In J. W. de Bakker and J. C. van Vliet, editors, Algorithmic Languages. Proceedings of the International Symposium on Algorithmic Languages, pages 345–372. North-Holland, Amsterdam, 1981. See Chapter 3.

    Google Scholar 

  18. E. Ritter and A. M. Pitts. A fully abstract translation between a A-calculus with reference types and Standard ML. In 2nd Int. Con f. on Typed Lambda Calculus and Applications, Edinburgh, 1995, volume 902 of Lecture Notes in Computer Science, pages 397–413. Springer-Verlag, Berlin, 1995.

    Google Scholar 

  19. D. S. Scott. A typetheoretical alternative to Cum, ISWIM, OwHY. Theoretical Computer Science, 121: 411–440, 1993.

    Article  MathSciNet  Google Scholar 

  20. K. Sieber. Full abstraction for the second order subset of an ALGOL-like language. Technical Report A 04/95, Fach. Informatik, Univ. des Saarlandes, Saarbrücken, Germany, April 1995. To appear in Information and Computation. See Chapter 15.

    Google Scholar 

  21. K. Sieber. Full abstraction via logical relations. Habilitationsschrift, FB 14 Informatik, Universität des Saarlandes, July 1995.

    Google Scholar 

  22. S. F. Smith. From operational to denotational semantics. In S. Brookes et al,editor, 7th International Conference on Mathematical Foundations of Programming Semantics, Pittsburgh PA, volume 598 of Lecture notes in Computer Science, pages 54–76. Springer-Verlag, Berlin, 1992.

    Google Scholar 

  23. I. D. B. Stark. Names and Higher-Order Functions. PhD thesis, University of Cambridge, 1994. Also published as Technical Report 363, University of Cambridge Computer Laboratory, April 1995.

    Google Scholar 

Download references

Authors
  1. Andrew M. Pitts
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dept. of Computer Science, Queen Mary & Westfield College, E1 4NS, England

    Peter W. O’Hearn

  2. Dept. of Computing and Information Science, Queen’s University, K7L 3N6, Kingston, Ontario, Canada

    Robert D. Tennent

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer Science+Business Media New York

About this chapter

Cite this chapter

Pitts, A.M. (1997). Reasoning About Local Variables with Operationally-Based Logical Relations. In: O’Hearn, P.W., Tennent, R.D. (eds) Algol-like Languages. Progress in Theoretical Computer Science. Birkhäuser, Boston, MA. https://doi.org/10.1007/978-1-4757-3851-3_7

Download citation

  • DOI: https://doi.org/10.1007/978-1-4757-3851-3_7

  • Publisher Name: Birkhäuser, Boston, MA

  • Print ISBN: 978-1-4757-3853-7

  • Online ISBN: 978-1-4757-3851-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation