Strictness analysis and denotational abstract interpretation

ABSTRACT

A theory of abstract interpretation [CoCo79] is developed for a typed &lgr;-calculus. The typed &lgr;-calculus is the “static” part of a two-level denotational metalanguage for which abstract interpretation was developed in [Nie86]. The present development relaxes a condition imposed in [Nie86] and this suffices to make the framework applicable to strictness analysis for the &lgr;-calculus. This shows the possibility of a general theory (and hence a system) for the analysis of functional programs. Furthermore, it gives more insight into the relative precision of the various analyses. In particular, it is shown that a collecting (static [CoCo79]) semantics exists, thus answering a problem left open in [BHA86].

REFERENCES

• Abr85: S.Abramsky: Strictness Analysis via Logical Relations, unpublished manuscript, 1985.
• BaMa83: R.Barbutl, A.Marte111: A Structural Approach to Static Semantics Correctness, Scl. of Comp. Proq., vol. 3, 1983.
• BHA86: G.L.Burn, C.L.Hankln, S.Abramsky: The Theory of Strictness Analysis for Higher Order Functions, Springer Lecture Notes in Computer Science, vol. 217, 1986. Also see Imperial College report ss/6.
• CoCo79: Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
• Hug86: J.Hughes: Strictness detection in non-flat domains, Springer Lecture Notes in Computer Science, vol. 217, 1986.
• JoMu81: N.D.Jones,S.S'Nuchnlck: Complexity of Flow Analysis, Inductive Assertion Synthesis and a Language due to Dijkstra, in: Program Flow Analysis: Theory and Applications, S.S.Muchnlck, N.D.Jones, (eds.), Prentice-Hall, 1981.
• JoMy86: Neil D. Jones , Alan Mycroft, Data flow analysis of applicative programs using minimal function graphs, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.296-306, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512672]
• Mau86: D.Maurer: Strictness computation using generalised A-expressions, Springer Lecture Notes in Computer Science, vol. 217, 1986.
• Myc81: A.Mycroft: Abstract interpretation and Optimizing Transformations for Applicative Programs, Ph.D.-thesis, Edinburgh, 1981.
• MyJo86: A.Mycroft, N.D.Jones: A relational framework for abstract interpretation, Springer Lecture Notes in Computer Science, vol. 217, 1986.
• MyNi83: Alan Mycroft , Flemming Nielson, Strong Abstract Interpretation Using Power Domains (Extended Abstract), Proceedings of the 10th Colloquium on Automata, Languages and Programming, p.536-547, July 18-22, 1983
• Nie82: F.Nielson: A Denotational Framework for Data Flow Analysi8, Acta Inf. vol. 18, 1982.
• Nie84: F.Nielson: Abstract Interpretation using Domain Theory, Ph.D.-thesl8, Edinburgh, 1984.
• Nie86: F Nielson, Abstract interpretation of denotational definitions, 3rd annual symposium on theoretical aspects of computer science on STACS 86, p.1-20, January 1986, Orsay, France
• Nie86a: F.Nielson: Strictness Analysis and Denotational Abstract Interpretation, report, Institute of Electronic Systems, Aalborg University Centre, Denmark, 1986.
• Rey74: On the Relation Between Direct and Continuation Semantics,2nd ICALP, Springer Lecture Notes in Computer Science, vol. 14, 1974.
• Sch86: David A. Schmidt, Denotational semantics: a methodology for language development, William C. Brown Publishers, Dubuque, IA, 1986

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.3 PROGRAMMING LANGUAGES

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

General Terms:
Algorithms, Languages, Theory