Journal of the ACM Bibliography

Abstract

We propose that the phenomenon of local state may be understood in terms of Strachey's concept of parametric (i.e., uniform) polymorphism. The intuitive basis for our proposal is the following analogy: a non-local procedure is independent of locally-declared variables in the same way that a parametrically polymorphic function is independent of types to which it is instantiated.

A connection between parametricity and representational abstraction was first suggested by J. C. Reynolds. Reynolds used logical relations to formalize this connection in languages with type variables and user-defined types. We use relational parametricity to construct a model for an Algol-like language in which interactions between local and non-local entities satisfy certain relational criteria. Reasoning about local variables essentially involves proving properties of polymorphic functions. The new model supports straightforward validations of all the test equivalences that have been proposed in the literature for local-variable semantics, and encompasses standard methods of reasoning about data representations. It is not known whether our techniques yield fully abstract semantics. A model based on partial equivalence relations on the natural numbers is also briefly examined. Copyright 1995 by ACM, Inc.

The abstract is also available as a LaTeX file, a DVI file, or a PostScript file.

Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theory -- semantics; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages -- denotational semantics

General Terms: Languages, Theory

Additional Key Words and Phrases: Algol-like languages, local state, logical relations, parametric polymorphism

Selected papers that cite this one

• Stephen Brookes. The essence of Parallel Algol. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pages 164-173, New Brunswick, New Jersey, 27-30 July 1996. IEEE Computer Society Press.

• David A. Naumann. A categorical model for higher order imperative programming. Mathematical Structures in Computer Science, 8(4):351-399, August 1998.

• Andrew M. Pitts. Reasoning about local variables with operationally-based logical relations. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pages 152-163, New Brunswick, New Jersey, 27-30 July 1996. IEEE Computer Society Press.

• Jon G. Riecke and Anders Sandholm. A relational account of call-by-value sequentiality. In Proceedings, Twelth Annual IEEE Symposium on Logic in Computer Science, pages 258-267, Warsaw, Poland, 29 June-2 July 1997. IEEE Computer Society Press.

• Kurt Sieber. Full abstraction for the second order subset of an ALGOL-like language. Theoretical Computer Science, 168(1):155-212, 10 November 1996.

• Mitchell Wand and Gregory T. Sullivan. Denotational semantics using an operationally-based term model. In Conference Record of POPL '97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 386-399, Paris, France, 15-17 January 1997.

Selected references

• Roberto M. Amadio. Recursion over realizability structures. Information and Computation, 91(1):55-85, March 1991.

• P. Freyd, P. Mulry, G. Rosolini, and D. Scott. Extensional PERs. In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pages 346-354, Philadelphia, Pennsylvania, 4-7 June 1990. IEEE Computer Society Press.

• P. J. Freyd, E. P. Robinson, and G. Rosolini. Functorial parametricity. In Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 444-452, Santa Cruz, California, 22-25 June 1992. IEEE Computer Society Press.

• Furio Honsell, Ian A. Mason, Scott Smith, and Carolyn Talcott. A variable typed logic of effects. Information and Computation, 119(1):55-90, 15 May 1995.

• Ian A. Mason and Carolyn L. Talcott. References, local variables and operational reasoning. In Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 186-197, Santa Cruz, California, 22-25 June 1992. IEEE Computer Society Press.

• Wesley Phoa. Effective domains and intrinsic structure. In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pages 366-377, Philadelphia, Pennsylvania, 4-7 June 1990. IEEE Computer Society Press.

• Andrew M. Pitts. Relational properties of recursively defined domains. In Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science, pages 86-97, Montreal, Canada, 19-23 June 1993. IEEE Computer Society Press.

• Uday S. Reddy. Passivity and independence. In Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 342-352, Paris, France, 4-7 July 1994. IEEE Computer Society Press.

• John C. Reynolds and Gordon D. Plotkin. On functors expressible in the polymorphic typed lambda calculus. Information and Computation, 105(1):1-29, July 1993.

• Edmund Robinson. How complete is PER? In Proceedings, Fourth Annual Symposium on Logic in Computer Science, pages 106-111, Asilomar Conference Center, Pacific Grove, California, 5-8 June 1989. IEEE Computer Society Press.

• E. P. Robinson and G. Rosolini. Reflexive graphs and parametric polymorphism. In Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 364-371, Paris, France, 4-7 July 1994. IEEE Computer Society Press.

• Robert Tennent. Semantical analysis of specification logic. Information and Computation, 85(2):135-162, April 1990.

Shortcuts: