Abstract
We present a denotational semantics for an Algol-like language, Alg, which is fully abstract for the second-order subset. This constitutes the first significant full-abstraction result for a block-structured language with local variables. As all the published ‘test equivalences’ [MS88, Len93, 0T95] for Algol-like languages are contained in the second-order subset, they can all be validated (easily) in our denotational model.
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
Arthur F. Lent. The category of functors from state shapes to bottomless epos is adequate for block structure. In Proc. ACM SIGPLAN Workshop on State in Programming Languages, Copenhagen, Denmark, pages 101–119, Technical report YALEU/DCS/RR-968, Department of Computer Science, Yale University, 1993.
Ralph Loader. The undecidability of A-definability. Mathematical Institute, Oxford University, June 1993.
Albert R. Meyer and Kurt Sieber. Towards fully abstract semantics for local variables: Preliminary report. In Proc. 15th Annual ACM Symp. on Principles of Programming Languages,San Diego, pages 191–203, ACM, 1988. See Chapter 7.
Peter W. O’Hearn and Robert D. Tennent. Parametricity and local variables. Journal of the ACM,42(3):658–709, 1995. See Chapter 16.
Gordon D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5: 223–256, 1977.
Andrew M. Pitts and Ian D. B. Stark. Observable properties of higher order functions that dynamically create local names, or: What’s new? In Andrzej M. Borzyszkowski and Stefan Sokolowski, editors, Proc. 18th International Symposium on Mathematical Foundations of Computer Science,Lecture Notes in Computer Science, volume 711, pages 122–141, Springer, 1993.
John C. Reynolds. The essence of ALGOL. In J. deBakker and van Vliet, editors, Int’1. Symp. Algorithmic Languages, pages 345–372. North-Holland, 1981. See Chapter 3.
Kurt Sieber. Reasoning about sequential functions via logical relations. In M. P. Fourman, P. T. Johnstone, and A. M. Pitts, editors, Applications of Categories in Computer Science, London Mathematical Society Lecture Note Series 177, pages 258–269. Cambridge University Press, 1992.
Kurt Sieber. Full abstraction for the second order subset of an ALGoL-like language. Theoretical Computer Science, 1996. To appear.
Stephen Weeks and Matthias Felleisen. On the orthogonality of assignments and procedures in ALGOL In Proc. 20th Annual ACM Symposium on Principles of Programming Languages,Charleston, pages 57–70, ACM, 1993. See Chapter 5.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer Science+Business Media New York
About this chapter
Cite this chapter
Sieber, K. (1997). Full Abstraction for the Second-Order Subset of an Algol-like Language. 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_5
Download citation
DOI: https://doi.org/10.1007/978-1-4757-3851-3_5
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