Global State Considered Unnecessary: Introduction to Object-Based Semantics

  • Uday S. Reddy
Part of the Progress in Theoretical Computer Science book series (PTCS)


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.


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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [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
  2. [Agh86]
    G. Agha. Actors: A Model of Concurrent Computation in Distributed Systems. The MIT Press, 1986.Google Scholar
  3. [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
  4. [AJ94]
    S. Abramsky and R. Jagadeesan. Games and full completeness for multiplicative linear logic. J. Symbolic Logic, 59 (2): 543–574, 1994.MathSciNetzbMATHCrossRefGoogle Scholar
  5. [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
  6. [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.zbMATHCrossRefGoogle Scholar
  7. [AR88]
    I. J. Aalbersberg and G. Rozenberg. Theory of traces. Theoretical Computer Science, 60: 1–82, 1988.MathSciNetzbMATHGoogle Scholar
  8. [Bar84]
    H. P. Barendregt. The Lambda Calculus, 2nd edition. North-Holland, 1984.Google Scholar
  9. [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
  10. [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
  11. [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
  12. [Bie93]
    G. M. Bierman. On Intuitionistic Linear Logic. PhD thesis, Computer Laboratory, University of Cambridge, December 1993.Google Scholar
  13. [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
  14. [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.MathSciNetzbMATHCrossRefGoogle Scholar
  15. [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
  16. [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
  17. [Gir87a]
    J.-Y. Girard. Linear logic. Theoretical Computer Science, 50: 1–102, 1987.MathSciNetzbMATHCrossRefGoogle Scholar
  18. Gir87b] J.-Y. Girard. Towards a geometry of interaction. In Gray and Scedrov [GS89], pages 69–108.Google Scholar
  19. [GLT89]
    J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989.Google Scholar
  20. [GS89]
    J. W. Gray and A. Scedrov, editors. Categories in Computer Science and Logic, volume 92 of Contemporary Mathematics, AMS, 1989.Google Scholar
  21. [Gun92]
    C. A. Gunter. Semantics of Programming Languages: Structures and Techniques. The MIT Press, 1992.Google Scholar
  22. [Gup94]
    V. Gupta. Chu Spaces: A Model of Concurrency. PhD thesis, Stanford University, August 1994.Google Scholar
  23. [Hen94]
    M. Hennessy. A fully abstract denotational model for higher-order processes. Information and Computation, 112 (1): 55–95, July 1994.MathSciNetzbMATHCrossRefGoogle Scholar
  24. [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
  25. [H094]
    J. M. E. Hyland and C.-H. L. Ong. On full abstraction for PCF (preliminary version). Manuscript, Cambridge University, October 1994.Google Scholar
  26. [Hoa69]
    C. A. R. Hoare. An axiomatic basis for computer programming. Comm. ACM, 12: 576–583, 1969.zbMATHCrossRefGoogle Scholar
  27. [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
  28. [Hoa72]
    C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1: 271–281, 1972.zbMATHCrossRefGoogle Scholar
  29. [Hoa85]
    C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall International, London, 1985.zbMATHGoogle Scholar
  30. [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
  31. [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
  32. [KM77]
    G. Kahn and D. B. MacQueen. Coroutines and networks of parallel processes. In Information Processing 77, pages 993–998, 1977.Google Scholar
  33. Lam87] J. Lambek. Multicategories revisited. In Gray and Scedrov [GS89].Google Scholar
  34. [Mac71]
    S. Mac Lane. Categories for the Working Mathematician. Springer-Verlag, 1971.Google Scholar
  35. [Maz77]
    A. Mazurkiewicz. Concurrent program schemes and their interpretations. DAIMI Report PB 78, Aarhus University, Aarhus, 1977.Google Scholar
  36. Maz89] A. Mazurkiewicz. Basic notions of trace theory. In de Bakker et al. dBdRR89], pages 285–363.Google Scholar
  37. 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
  38. [Mí189]
    R. Milner. Communication and Concurrency. Prentice Hall, 1989.Google Scholar
  39. [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
  40. [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
  41. 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
  42. [O’H90]
    P. W. O’Hearn. Semantics of Noninterference: A Natural Approach. PhD thesis, Queen’s University, Kingston, Canada, 1990.Google Scholar
  43. [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
  44. [O’H93]
    P. W. O’Hearn. A model for syntactic control of interference. Mathematical Structures in Computer Science, 3: 435–465, 1993.MathSciNetzbMATHCrossRefGoogle Scholar
  45. [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
  46. 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
  47. OR95] P. W. O’Hearn and U. S. Reddy. Objects, interference and the Yoneda embedding. In Brookes et al. [BMMM95].Google Scholar
  48. [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
  49. [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
  50. [OT93]
    P. W. O’Hearn and R. D. Tennent. Semantical analysis of specification logic, 2. Information and Computation, 107 (1): 25–57, 1993.MathSciNetzbMATHCrossRefGoogle Scholar
  51. OT95] P. W. O’Hearn and R. D. Tennent. Parametricity and local variables. J. ACM, 42(3), 1995. See Chapter 16.Google Scholar
  52. [PL95]
    S. L. Peyton Jones and J. Launchbury. State in HASKELL. LISP and Symbolic Computation, 8 (4): 293–341, 1995.Google Scholar
  53. [P1077]
    G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5: 223–255, 1977.MathSciNetGoogle Scholar
  54. [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
  55. [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
  56. 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
  57. [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
  58. [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
  59. [Red93b]
    U. S. Reddy. A linear logic model of state. Electronic manuscript, University of Illinois (anonymous FTP from, October 1993.Google Scholar
  60. [Red93c]
    U. S. Reddy. A linear logic model of state (extended abstract). Technical report, University of Glasgow, January 1993.Google Scholar
  61. [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
  62. [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
  63. 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
  64. [Rey8la]
    J. C. Reynolds. The Craft of Programming. Prentice-Hall International, London, 1981.zbMATHGoogle Scholar
  65. [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
  66. [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
  67. [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
  68. [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
  69. [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
  70. [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
  71. [Sha87]
    E. Shapiro. CONCURRENT PROLOG: Collected Papers. The MIT Press, 1987. ( Two volumes).Google Scholar
  72. [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
  73. [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
  74. [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
  75. [Sto77]
    J. E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. The MIT Press, 1977.Google Scholar
  76. [Ten83]
    R. D. Tennent. Semantics of interference control. Theoretical Computer Science, 27: 297–310, 1983.MathSciNetzbMATHGoogle Scholar
  77. [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
  78. Ten90] R. D. Tennent. Semantical analysis of specification logic. Information andComputation,85(2):135–162, 1990. See Chapter 13.Google Scholar
  79. [Ten91]
    R. D. Tennent. Semantics of Programming Languages. Prentice-Hall International, London, 1991.Google Scholar
  80. [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
  81. [Weg87]
    P. Wegner. Dimensions of object-based language design. In Object Oriented Programming Systems, Languages and Applications. ACM SIGPLAN, 1987.Google Scholar
  82. [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
  83. [Win89]
    G. Winskel. An introduction to event structures. In de Bakker et al.Google Scholar
  84. [dBdRR89]
    pages 364–397.Google Scholar
  85. [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
  86. [Zha91]
    G.-Q. Zhang. Logic of Domains. Birkhäuser, Boston, 1991.Google Scholar
  87. [Zha93]
    G.-Q. Zhang. Some monoidal closed categories of stable domains and event structures. Mathematical Structures in Computer Science, 3: 259–276, 1993.zbMATHCrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media New York 1997

Authors and Affiliations

  • Uday S. Reddy

There are no affiliations available

Personalised recommendations