Full Abstraction for the Second-Order Subset of an Algol-like Language
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.
KeywordsLocal Variable Procedure Call Denotational Semantic Ground Type Mathematical Society Lecture Note Series
Unable to display preview. Download preview PDF.
- [Len93]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.Google Scholar
- [Loa93]Ralph Loader. The undecidability of A-definability. Mathematical Institute, Oxford University, June 1993.Google Scholar
- [MS88]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.Google Scholar
- [OT95]Peter W. O’Hearn and Robert D. Tennent. Parametricity and local variables. Journal of the ACM,42(3):658–709, 1995. See Chapter 16.Google Scholar
- [PS93]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.Google Scholar
- [Rey81]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.Google Scholar
- [Sie92]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.Google Scholar
- [Sie96]Kurt Sieber. Full abstraction for the second order subset of an ALGoL-like language. Theoretical Computer Science, 1996. To appear.Google Scholar
- [WF93]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.Google Scholar