Algol-like Languages pp 227-295 | Cite as

# Global State Considered Unnecessary: Introduction to Object-Based Semantics

Chapter

## Abstract

Semantics of imperative programming languages is traditionally described in terms of functions on global states. We propose here a novel approach based on a notion of *objects* and characterize them in terms of their observable behavior. States are regarded as part of the internal structure of objects and play no role in the observable behavior. It is shown that this leads to considerable accuracy in the semantic modelling of locality and single-threadedness properties of objects.

## Keywords

Object Space Linear Logic Consistency Relation Storage Cell Lambda Calculus
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

## Preview

Unable to display preview. Download preview PDF.

## References

- [Abr94]S. Abramsky. Interaction categories and communicating sequential processes. In A. W. Roscoe, editor, A
*Classical Mind: Essays in Honor of C*. A.*R. Hoare*, pages 1–16. Prentice-Hall International, 1994.Google Scholar - [Agh86]G. Agha.
*Actors: A Model of Concurrent Computation in Distributed Systems*. The MIT Press, 1986.Google Scholar - [AJ92]S. Abramsky and R. Jagadeesan. New foundations for geometry of interaction. In
*Proceedings*,*Seventh Annual IFFF Symposium on Logic in Computer Science*, pages 211–222. JFFF Computer Society Press, June 1992.CrossRefGoogle Scholar - [AJ94]S. Abramsky and R. Jagadeesan. Games and full completeness for multiplicative linear logic.
*J. Symbolic Logic*, 59 (2): 543–574, 1994.MathSciNetMATHCrossRefGoogle Scholar - [AJM94]S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF (extended abstract). In M. Hagiya and J. C. Mitchell, editors,
*Theoretical Aspects of Computer Software*, volume 789 of*Lecture Notes in Computer Science*, pages 1–15. Springer-Verlag, 1994.Google Scholar - [Apt81]K. R. Apt. Ten years of Hoare’s logic: A survey.
*ACM Transactions on**Programming Languages and Systems*, 3 (4): 431–483, October 1981.MATHCrossRefGoogle Scholar - [AR88]I. J. Aalbersberg and G. Rozenberg. Theory of traces.
*Theoretical Computer**Science*, 60: 1–82, 1988.MathSciNetMATHGoogle Scholar - [Bar84]H. P. Barendregt.
*The Lambda Calculus*, 2nd edition. North-Holland, 1984.Google Scholar - [BBdPH92]P. N. Benton, G. M. Bierman, V. C. V. de Paiva, and J. M. E. Hyland.
*Term Assignment for Intuitionistic Linear Logic*. Technical Report 262, Computer Laboratory, University of Cambridge, August 1992.Google Scholar - [Ber78]G. Berry. Stable models of typed A-calculi. In
*Fifth International Colloquium**on Automata*,*Languages and Programming*, volume 62 of*Lecture Notes in Computer Science*, pages 72–88. Springer-Verlag, 1978.Google Scholar - [BG90]C. Brown and D. Gurr. A categorical linear framework for Petri nets. In
*Proceedings*,*Fifth Annual IEEE Symposium on Logic in Computer Science*, pages 208–218. IFFF Computer Society Press, June 1990.CrossRefGoogle Scholar - [Bie93]G. M. Bierman.
*On Intuitionistic Linear Logic*. PhD thesis, Computer Laboratory, University of Cambridge, December 1993.Google Scholar - [BMMM95]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*Elsevier, 1995.Google Scholar - [CCF94]R. Cartwright, P.-L. Curien, and M. Felleisen. Fully abstract semantics for observably sequential languages.
*Information and Computation*, 111 (2): 297–401, June 1994.MathSciNetMATHCrossRefGoogle Scholar - [dBdRR89]J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors.
*Linear Time*,*Branching Time and Partial Order in Logics and Models of Concurrency*, volume 354 of*Lecture Notes in Computer Science*. Springer-Verlag, 1989.Google Scholar - [FW79]D. P. Freidman and D. S. Wise. An approach to fair applicative multiprogramming. In G. Kahn, editor,
*Semantics of Concurrent Computation*, volume 70 of*Lecture Notes in Computer Science*, pages 203–226. Springer-Verlag, 1979.Google Scholar - [Gir87a]J.-Y. Girard. Linear logic.
*Theoretical Computer Science*, 50: 1–102, 1987.MathSciNetMATHCrossRefGoogle Scholar - Gir87b] J.-Y. Girard. Towards a geometry of interaction. In Gray and Scedrov [GS89], pages 69–108.Google Scholar
- [GLT89]J.-Y. Girard, Y. Lafont, and P. Taylor.
*Proofs and Types*. Cambridge University Press, 1989.Google Scholar - [GS89]J. W. Gray and A. Scedrov, editors.
*Categories in Computer Science and**Logic*, volume 92 of*Contemporary Mathematics*, AMS, 1989.Google Scholar - [Gun92]C. A. Gunter.
*Semantics of Programming Languages: Structures and Techniques*. The MIT Press, 1992.Google Scholar - [Gup94]V. Gupta.
*Chu Spaces: A Model of Concurrency*. PhD thesis, Stanford University, August 1994.Google Scholar - [Hen94]M. Hennessy. A fully abstract denotational model for higher-order processes.
*Information and Computation*, 112 (1): 55–95, July 1994.MathSciNetMATHCrossRefGoogle Scholar - [HMT83]J. Y. Halpern, A. R. Meyer, and B. A. Trahktenbrot. The semantics of local storage, or what makes the free list free? In
*Tenth Annual ACM Symposium on Principles of Programming Languages*, pages 245–257. ACM, 1983.Google Scholar - [H094]J. M. E. Hyland and C.-H. L. Ong. On full abstraction for PCF (preliminary version). Manuscript, Cambridge University, October 1994.Google Scholar
- [Hoa69]C. A. R. Hoare. An axiomatic basis for computer programming.
*Comm. ACM*, 12: 576–583, 1969.MATHCrossRefGoogle Scholar - [Hoa71]C. A. R. Hoare. Procedures and parameters: An axiomatic approach. In E. Engeler, editor,
*Symposium on Semantics of Algorithmic Languages*, volume 188 of*Lecture Notes in Mathematics*, pages 102–116. Springer-Verlag, 1971.Google Scholar - [Hoa72]C. A. R. Hoare. Proof of correctness of data representations.
*Acta Informatica*, 1: 271–281, 1972.MATHCrossRefGoogle Scholar - [Hoa85]C. A. R. Hoare.
*Communicating Sequential Processes*. Prentice-Hall International, London, 1985.MATHGoogle Scholar - [JM91]T. Jim and A. R. Meyer. Full abstraction and the context lemma. In T. Ito and A. R. Meyer, editors,
*Theoretical Aspects of Computer Software*, volume 526 of*Lecture Notes in Computer Science*, pages 131–151. Springer-Verlag, 1991.Google Scholar - [KL85]R. M. Keller and G. Lindstrom. Approaching distributed database implementations through functional programming concepts. In
*International**Conference on Distributed Computing Systems*. IFEF, May 1985.Google Scholar - [KM77]G. Kahn and D. B. MacQueen. Coroutines and networks of parallel processes. In
*Information Processing*77, pages 993–998, 1977.Google Scholar - Lam87] J. Lambek. Multicategories revisited. In Gray and Scedrov [GS89].Google Scholar
- [Mac71]S. Mac Lane.
*Categories for the Working Mathematician*. Springer-Verlag, 1971.Google Scholar - [Maz77]A. Mazurkiewicz. Concurrent program schemes and their interpretations. DAIMI Report PB 78, Aarhus University, Aarhus, 1977.Google Scholar
- Maz89] A. Mazurkiewicz. Basic notions of trace theory. In de Bakker et al. dBdRR89], pages 285–363.Google Scholar
- Mí171] R. Milner. An algebraic definition of simulation between programs. In
*Proc.Second International Joint Conference on Artificial Intelligence*,pages 481489, London, 1971. The British Computer Society.Google Scholar - [Mí189]R. Milner.
*Communication and Concurrency*. Prentice Hall, 1989.Google Scholar - [Mit90]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 - [MS88]A. R. Meyer and K. Sieber. Towards fully abstract semantics for local variables. In
*Fifteenth Annual ACM Symposium on Principles of Programming Languages*, pages See Chapter 7. 191–203. ACM, 1988.Google Scholar - Nau60] P. Naur (editor), J. W. Backus, et al. Report on the algorithmic language ALGOL 60.
*Comm*. ACM, 3(5):299–314, May 1960.*Uday S. Reddy*285Google Scholar - [O’H90]P. W. O’Hearn.
*Semantics of Noninterference: A Natural Approach*. PhD thesis, Queen’s University, Kingston, Canada, 1990.Google Scholar - [O’H91]P. W. O’Hearn. Linear logic and interference control. In
*Category Theory**and Computer Science*, volume 350 of*Lecture Notes in Computer Science*, pages 74–93. Springer-Verlag, 1991.Google Scholar - [O’H93]P. W. O’Hearn. A model for syntactic control of interference.
*Mathematical**Structures in Computer Science*, 3: 435–465, 1993.MathSciNetMATHCrossRefGoogle Scholar - [O1e85]F. J. Oles. Type algebras, functor categories and block structure. In M. Nivat and J. C. Reynolds, editors,
*Algebraic Methods in Semantics*, pages 543–573. Cambridge University Press, 1985. See Chapter 11.Google Scholar - OPTT95] P. W. O’Hearn, A. J. Power, M. Takeyama, and R. D. Tennent. Syntactic control of interference revisited. In Brookes et al. [BMMM95]. See Chapter 18.Google Scholar
- OR95] P. W. O’Hearn and U. S. Reddy. Objects, interference and the Yoneda embedding. In Brookes et al. [BMMM95].Google Scholar
- [ORH93]M. Odersky, D. Rabin, and P. Hudak. Call by name, assignment and the lambda calculus. In
*Twentieth Annual ACM Symposium on Principles of Programming Languages*ACM, 1993.Google Scholar - [OT92]P. W. O’Hearn and R. D. Tennent. Semantics of local variables. In M. P. Four- man, P. T. Johnstone, and A. M. Pitts, editors,
*Applications of Categories in Computer Science*, pages 217–238. Cambridge University Press, 1992.Google Scholar - [OT93]P. W. O’Hearn and R. D. Tennent. Semantical analysis of specification logic, 2.
*Information and Computation*, 107 (1): 25–57, 1993.MathSciNetMATHCrossRefGoogle Scholar - OT95] P. W. O’Hearn and R. D. Tennent. Parametricity and local variables.
*J. ACM*, 42(3), 1995. See Chapter 16.Google Scholar - [PL95]S. L. Peyton Jones and J. Launchbury. State in HASKELL.
*LISP and Symbolic**Computation*, 8 (4): 293–341, 1995.Google Scholar - [P1077]G. D. Plotkin. LCF considered as a programming language.
*Theoretical**Computer Science*, 5: 223–255, 1977.MathSciNetGoogle Scholar - [Pra84]V. Pratt. The pomset model of parallel processes: Unifying the temporal and the spatial. In
*Seminar on Concurrency*, volume 197 of*Lecture Notes in Computer Science*, pages 180–196. Springer-Verlag, 1984.Google Scholar - [PT93]B. C. Pierce and D. N. Turner. Object-oriented programming without recursive types. In
*Twentieth Annual ACM Symposium on Principles of Programming Languages*, pages 299–312. ACM, 1993.Google Scholar - PW93] S. L. Peyton Jones and P. Wadler. Imperative functional programming In
*Twentieth Annual ACM Symposium on Principles of Programming Languages*,pages 71–84, ACM, 1993.Google Scholar - [PW94]G. Plotkin and G. Winskel. Bistructures, bidomains and linear logic. In
*ICALP ‘84*, volume 820 of*Lecture Notes in Computer Science*. Springer-Verlag, 1994.Google Scholar - [Red93a]U. S. Reddy. Global state considered unnecessary: Semantics of interference-free imperative programming. In
*ACM SIGPLAN Workshop on State in Programming Languages*, pages 120–135. Technical Report YALEU/DCS/RR-968, June 1993.Google Scholar - [Red93b]U. S. Reddy. A linear logic model of state. Electronic manuscript, University of Illinois (anonymous FTP from cs.uiuc.edu), October 1993.Google Scholar
- [Red93c]U. S. Reddy. A linear logic model of state (extended abstract). Technical report, University of Glasgow, January 1993.Google Scholar
- [Red94]U. S. Reddy. Passivity and independence. In
*Proceedings*,*Ninth Annual IFFF**Symposium on Logic in Computer Science*, pages 342–352 IFFF Computer Society Press, July 1994.CrossRefGoogle Scholar - [Ret93]C. Retoré.
*Réseaux et Séquents Ordonnés*. Thèse de Doctorat, spécialité Mathématiques, Université Paris 7, February 1993. ( English translation available from the author).Google Scholar - Rey78] J. C. Reynolds. Syntactic control of interference. In
*ACM Symposium onPrinciples of Programming Languages*,pages 39–46. ACM, 1978. See Chapter 10.Google Scholar - [Rey8la]J. C. Reynolds.
*The Craft of Programming*. Prentice-Hall International, London, 1981.MATHGoogle Scholar - [Rey81b]J. C. Reynolds. The essence of ALGOL In J. W. de Bakker and J. C. van Vliet, editors,
*Algorithmic Languages*, pages 345–372. North-Holland, 1981. See Chapter 3.Google Scholar - [Rey82]J. C. Reynolds. IDEALIZED ALGOL and its specification logic. In D. Néel, editor,
*Tools and Notions for Program Construction*, pages 121–161. Cambridge University Press, 1982. See Chapter 6.Google Scholar - [Rey88]J. C. Reynolds.
*Preliminary Design of the Programming Language FORSYTHE*. Technical Report CMU-CS-88–159, Carnegie-Mellon University, June 1988. See Chapter 8.Google Scholar - [Rey89]J. C. Reynolds. Syntactic control of interference, Part II. In
*Automata*,*Languages and Programming*,*16th International Colloquium*, volume 372 of*Lecture Notes in Computer Science*, pages 704–722. Springer-Verlag, 1989.Google Scholar - [RK94]U. S. Reddy and S. N. Kamin. Two semantic models of object-oriented languages. In C. A. Gunter and J. C. Mitchell, editors,
*Theoretical Aspects of Object-Oriented Programming*, pages 463–496. The MIT Press, 1994.Google Scholar - [Sco80]D. S. Scott. Relating theories of the lambda calculus. In
*To H. B. Curry*:*Essays on Combinatory Logic*,*Lambda Calculus and Formalism*, pages 403450. Academic Press, 1980.Google Scholar - [Sha87]E. Shapiro.
*CONCURRENT PROLOG: Collected Papers*. The MIT Press, 1987. ( Two volumes).Google Scholar - [Sie93]K. Sieber. New steps towards full abstraction for local variables. In
*ACM**SIGPLAN Workshop on State in Programming Languages*, pages 88–100. Technical Report YALEU/DCS/RR-968, Yale University, New Haven, 1993.Google Scholar - [Sie94]K. Sieber. Full Abstraction for the Second Order Subset of an ALGOL-like Language (preliminary report). Technical Bericht A 01/94, Universitaet des Saarlandes, Saarbruecken, February 1994. See Chapter 15.Google Scholar
- [SRI91]V. Swamp, U. S. Reddy, and E. Ireland. Assignments for applicative languages. In R. J. M. Hughes, editor,
*Con f. on Functional Programming Languages and Computer Architecture*, volume 523 of*Lecture Notes in Computer Science*, pages 192–214. Springer-Verlag, 1991. See Chapter 9.Google Scholar - [Sto77]J. E. Stoy.
*Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory*. The MIT Press, 1977.Google Scholar - [Ten83]R. D. Tennent. Semantics of interference control.
*Theoretical Computer**Science*, 27: 297–310, 1983.MathSciNetMATHGoogle Scholar - [Ten95]R. D. Tennent. Denotational semantics. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors,
*Handbook of Logic in Computer Science*, volume 3, pages 169–322, Oxford University Press, 1995.Google Scholar - Ten90] R. D. Tennent. Semantical analysis of specification logic.
*Information andComputation*,85(2):135–162, 1990. See Chapter 13.Google Scholar - [Ten91]R. D. Tennent.
*Semantics of Programming Languages*. Prentice-Hall International, London, 1991.Google Scholar - [Wad91]P. Wadler. Is there a use for linear logic?
*In Proc. Symposium on Partial Evaluation and Semantics-Based Program Manipulation*, pages 255–273. ACM, 1991. ( SIGPLAN Notices, Sept. 1991 ).Google Scholar - [Weg87]P. Wegner. Dimensions of object-based language design. In
*Object Oriented Programming Systems*,*Languages and Applications*. ACM SIGPLAN, 1987.Google Scholar - [WF93]S. Weeks and M. Felleisen. On the orthogonality of assignments and procedures in ALGOL. In
*Twentieth Annual ACM Symposium on Principles of Programming Languages*,pages 57–70, ACM, 1993. See Chapter 5.Google Scholar - [Win89]G. Winskel. An introduction to event structures. In de Bakker et al.Google Scholar
- [dBdRR89]pages 364–397.Google Scholar
- [Win94]G. Winskel. Stable bistructure models of PCF. In
*Mathematical Foundations**of Computer Science*, volume 841 of*Lecture Notes in Computer Science*. Springer-Verlag, 1994.Google Scholar - [Zha91]G.-Q. Zhang.
*Logic of Domains*. Birkhäuser, Boston, 1991.Google Scholar - [Zha93]G.-Q. Zhang. Some monoidal closed categories of stable domains and event structures.
*Mathematical Structures in Computer Science*, 3: 259–276, 1993.MATHCrossRefGoogle Scholar

## Copyright information

© Springer Science+Business Media New York 1997