The semantics of local storage, or what makes the free-list free?(Preliminary Report)

ABSTRACT

Denotational semantics for an ALGOL-like language with finite-mode procedures, blocks with local storage, and sharing (aliasing) is given by translating programs into an appropriately typed &lgr;-calculus. Procedures are entirely explained at a purely functional level - independent of the interpretation of program constructs - by continuous models for &lgr;-calculus. However, the usual (cpo) models are not adequate to model local storage allocation for blocks because storage overflow presents an apparent discontinuity. New domains of store models are offered to solve this problem.

REFERENCES

• 1: H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, Studies in Logic 103, North Holland, 1981.
• 2: B. Courcelle, Fundamental properties of infinite trees, Theoretical Computer Science25, 1983, 95-170.
• 3: W. Damm, The IO- and OI-hierarchies, Theoretical Computer Science20, 1982, 95-207.
• 4: W. Damm and E. Fehr, A schematological approach to the procedure concept of ALGOL-like languages, Proc. 5ieme colloque sur les arbres en algebre et en programmation, Lille, 1980, 130-134.
• 5: J. W. de Bakker, Mathematical Theory of Program Correctness, Prentice-Hall, Inc., Upper Saddle River, NJ, 1980
• 6: J. H. Gallier, n-Rational algebras, Parts I and II, Technical Report, Dept. of Computer and Information Sciences, Univ. of Pennsylvania, Philadelphia, 1983, 55pp. and 65pp.
• 7: Michael J. C. Gordon, The Denotational Description of Programming Languages: An Introduction, Springer-Verlag New York, Inc., Secaucus, NJ, 1979
• 8: Irene Guessarian, Algebraic Semantics, Springer-Verlag New York, Inc., Secaucus, NJ, 1981
• 9: I. Guessarian, Survey on some classes of interpretations and some their applications, Laboratoire Informatique Theorique et Programmation, 82-46, Univ. Paris 7, 1982.
• 10: Joseph Y. Halpern, A good Hoare axiom system for an ALGOL-like language, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.262-271, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800538]
• 11: R. Hindley, B. Lercher, and J. Seldin, Introduction to Combinatory Logic, London Math. Soc. Lecture Note Series 7, Cambridge University Press, 1972.
• 12: J. Lambek, From &lgr;-calculus to Cartesian closed categories, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. P. Seldin and J. R. Hindley, eds., Academic Press, 1980, 375-402.
• 13: P. J. Landin, Correspondence between ALGOL 60 and Church's Lambda-notation: part I, Communications of the ACM, v.8 n.2, p.89-101, Feb. 1965 [doi>10.1145/363744.363749]
• 14: Hans Langmaack , Ernst-Rüdiger Olderog, Present-Day Hoare-Like Systems for Programming Languages with Procedures: Power, Limits and most Likely Expressions, Proceedings of the 7th Colloquium on Automata, Languages and Programming, p.363-373, July 14-18, 1980
• 15: J. Meseguer, Completions, factorizations and colimits of &ohgr;-posets, Coll. Math. Soc. Janos Bolyai 26. Math. Logic in Computer Science, Salgotarjan, Hungary, 1978, 509-545.
• 16: A. R. Meyer, What is a model of the &lgr;-calculus? Information and Control52, 1982, 87-122.
• 17: Robert Milne , C. Strachey, A Theory of Programming Language Semantics, Halsted Press, New York, NY, 1977
• 18: P. Naur et al., Revised report on the algorithmic language ALGOL 60, Computer J. 5, 1963, 349-367.
• 19: M. Nivat, On the interpretation of recursive polyadic program schemes, Symposia Mathematica, 15, Academic Press, 1975, 255-281.
• 20: E. R. Olderog, Sound and complete Hoare-like calculi based on copy rules, Acta Informatica16, 1981, 161-197.
• 21: F. J. Oles, Type algebras, functor categories, and block structure, Computer Science Dept, Aarhus Univ. DAIMI PB-156, Denmark, Jan. 1983.
• 22: G. D. Plotkin, A powerdomain construction, SIAM J. Comp. 5, 1976, 452-487, 1976.
• 23: G. D. Plotkin, Lambda-definability in the full type hierarchy, in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. P. Seldin and J. R. Hindley, eds., Academic Press, 1980, 363-373.
• 24: Gordon D. Plotkin, A Powerdomain for Countable Non-Determinism (Extended Abstract), Proceedings of the 9th Colloquium on Automata, Languages and Programming, p.418-428, July 12-16, 1982
• 25: J. C. Reynolds, The essence of ALGOL, International Symposium on Algorithmic Languages, de Bakker and van Vliet, eds., North Holland, 1981a, 345-372.
• 26: John C. Reynolds, The Craft of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 27: J. C. Reynolds, Idealized ALGOL and its specification logic, Syracuse University, Technical Report 1-81, 1981c.
• 28: D. S. Scott, Lectures on a Mathematical Theory of Computation, Technical Monograph PRG-19, Oxford Univ. Computing Lab., 1981.
• 29: Dana S. Scott, Domains for Denotational Semantics, Proceedings of the 9th Colloquium on Automata, Languages and Programming, p.577-613, July 12-16, 1982
• 30: M. B. Smyth, Powerdomains, J. Computer and System Sciences16, 1978, 23-36.
• 31: R. Statman, Logical relations and the typed lambda-calculus, to appear, 1982.
• 32: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977
• 33: R. D. Tennent, Principles of Programming Languages, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 34: Boris A. Trakhtenbrot , Joseph Y. Halpern , Albert R. Meyer, From Denotational to Operational and Axiomatic Semantics for ALGOL-like Languages: an Overview, Proceedings of the Carnegie Mellon Workshop on Logic of Programs, p.474-500, June 06-08, 1983

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Denotational semantics

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.2 Storage Management
          Subjects: Allocation/deallocation strategies

General Terms:
Management