A calculus for assignments in higher-order languages

ABSTRACT

Imperative assignments are abstractions of recurring programming patterns in purely functional programming languages. When added to higher-order functional languages, they provide a higher-level of modularity and security but invalidate the simple substitution semantics. We show that, given an operational interpretation of a denotational semantics for such a language, it is possible to design a two-level extension of the &lgr;u-calculus. This calculus provides a location-free rewriting semantics of the language and offers new possibilities for reasoning with assignments. The upper level of the calculus factors out all the steps in a reduction sequence which must be in a linear order; the lower level allows a partial ordering of reduction steps.

REFERENCES

• 1: S Kamal Abdali , David S. Wise, Standard, storeless semantics for ALGOL-style block structure and call-by-name, Proceedings of the international conference on Mathematical foundations of programming semantics, p.1-19, October 1986, Manhattan
• 2: BARENDREGT, H.P. The Lambda Calculus: Its Syntaz and Semantics, North-Holland, Amsterdam, 1981.
• 3: Stephen D Brookes, A fully abstract semantics and a proof system for an ALGOL-like language with sharing, Proceedings of the international conference on Mathematical foundations of programming semantics, p.59-100, October 1986, Manhattan
• 4: DZ BRUIJN. N.G. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with applications to the Church-Rosser theorem, Indagationes Mathematics 37, 1972, 381- 392.
• 5: DONAHUZ, J.E. Locations considered unnecessary, Acta Inlormatiea 8, 1977, 221-242.
• 6: FZLLEISEN, S., D.P. FRIEDMAN. Control operators, the SECD-machine, and the A-calculus, Formal Description of Programming Concepts III, North- Holland, Amsterdam, 1986, to appear.
• 7: Joseph Y. Halpern , Albert R. Meyer , B. A. Trakhtenbrot, The semantics of local storage, or what makes the free-list free?(Preliminary Report), Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.245-257, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800536]
• 8: 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]
• 9: MASON, I. A. Equivalences of first-order Lisp programs, Proc. First S!tmp. Logic in Computer Science, 1986, 105-117.
• 10: James H. Morris, Jr., Protection in programming languages, Communications of the ACM, v.16 n.1, p.15-21, Jan. 1973 [doi>10.1145/361932.361937]
• 11: PLOTKIN, G .D. A structural approach to operational semantics, Tech. Rpt. DAIMI FN-19, Aarhus University, Computer Science Department, 1981.
• 12: PLOTKIN, G. D. Call-by-name, call-by-value, and the A-calculus, Theoretical Computer Science 1, 1975, 125-159.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Very high-level languages

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Algebraic approaches to semantics
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs

General Terms:
Algorithms, Languages, Standardization, Theory