In-place updates in the presence of control operators

ABSTRACT

This paper presents a formal account of the concept of in-place updates in purely functional languages. In purely functional languages, updates of abstract objects involve creating duplicates of these objects. This paper reviews static conditions, which, if satisfied by &lgr;-terms, guarantee that, even if updates are performed in-place, the purely functional semantics is retained. These static conditions, however, fail to guarantee the requisite safety in the presence of control operators like callcc and throw. The conditions are hence augmented by another condition which is defined on the operational semantics. Here we statically verify the satisfiability of a conservative approximation of this condition by data-flow analysis on CPS-terms. Also a significant class of programs is identified for which the condition holds even without data-flow analysis.

REFERENCES

• 1: Andrew W. Appel, Compiling with continuations, Cambridge University Press, New York, NY, 1992
• 2: Carl A. Gunter, Semantics of programming languages: structures and techniques, MIT Press, Cambridge, MA, 1992
• 3: Paul Hudak, A semantic model of reference counting and its abstraction (detailed summary), Proceedings of the 1986 ACM conference on LISP and functional programming, p.351-363, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319876]
• 4: P. Hudak. Mutable abstract datatypes. Technical Report YALEU/DCS/RR-914, Yale University, 1993.
• 5: Paul Hudak , Jonathan Young, Higher-order strictness analysis in untyped lambda calculus, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-109, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512653]
• 6: P. Curien R. Cartwright and M.Felleisen. Fully abstract models of observably sequential languages. Technical Report TR93-219, Rice University, 1993.
• 7: Jean-Claude Raoult , Ravi Sethi, The global storage needs of a subcomputation, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.148-157, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800526]
• 8: David A. Schmidt, Detecting global variables in denotational specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.2, p.299-310, April 1985 [doi>10.1145/3318.3323]
• 9: O. Shivers, Control flow analysis in scheme, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.164-174, June 20-24, 1988, Atlanta, Georgia, United States
• 10: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977
• 11: A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Technical Report COMP TR91-160, Department of Computer, Rice University, 1991.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Optimization

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Denotational semantics; Operational semantics
      F.3.3 Studies of Program Constructs
          Subjects: Control primitives
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Algorithms, Languages, Theory, Verification