Automatic binding time analysis for a typed &lgr;-calculus

ABSTRACT

For a typed &lgr;-calculus we develop an algorithm that, given some partial information about what must happen at run-time, will work out what actually can be computed at compile-time and what must be deferred to run-time.

REFERENCES

• 1: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 2: John Backus, Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs, Communications of the ACM, v.21 n.8, p.613-641, Aug. 1978 [doi>10.1145/359576.359579]
• 3: R. M. Burstall , D. B. MacQueen , D. T. Sannella, HOPE: An experimental applicative language, Proceedings of the 1980 ACM conference on LISP and functional programming, p.136-143, August 25-27, 1980, Stanford University, California, United States [doi>10.1145/800087.802799]
• 4: Pierre-Louis Curien, Categorical combinators, sequential algorithms, and functional programming (2nd ed.), Birkhauser Boston Inc., Cambridge, MA, 1994
• 5: R.Harper, D.MacQueen, R.Milner: Standard ML, Report, Edinburgh University, 1986.
• 6: Matthew S. Hecht, Flow Analysis of Computer Programs, Elsevier Science Inc., New York, NY, 1977
• 7: Neil D. Jones , S. S. Muchnick, Tempo: A Unified Treatment of Binding Time and Parameter Passing Concepts in Programming Languages, Springer-Verlag New York, Inc., Secaucus, NJ, 1978
• 8: R.Milner: A theory of type polymorphism in programming, JCSS, 1978.
• 9: 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
• 10: Hanne R. Nielson , Flemming Neilson, Semantics directed compiling for functional languages, Proceedings of the 1986 ACM conference on LISP and functional programming, p.249-257, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319867]
• 11: F. Nielson, Strictness analysis and denotational abstract interpretation, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.120-131, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41636]
• 12: F.Nielson: Towards a denotationul theory of abstract interpretation, to appear in: Abstract Interpretation of Declarative Languages (eds: S.Abramsky, C.Hankin).
• 13: Flemming Nielson , Hanne Riis Nielson, Two-level semantics and code generation, Theoretical Computer Science, v.56 n.1, p.59-133, Jan. 1988 [doi>10.1016/0304-3975(86)90006-X]
• 14: F.Nielson: A formal type system for comparing partial evaluators, Technical University of Denmark, May 1987. To be presented at Workshop on Partial Evaluation and Mixed Computation, Ebberup, Denmark, October, 1987.
• 15: H.R.Nielson, F.Nielsoa: Automatic bindiag time analysis for a typed A-calculus, Aalborg University Center, May 1987. 'Submitted for publication.
• 16: D.A.Schmidfi: Static properties of partial reduction, Kansas State University, 1987. To be presented at Workshop on Partial Evaluation and Mixed Computation, Ebberup, Denmark, October, 1987.
• 17: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977
• 18: D. A. Turner, Miranda: a non-strict functional language with polymorphic types, Proc. of a conference on Functional programming languages and computer architecture, p.1-16, January 1985, Nancy, France

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

General Terms:
Algorithms, Languages, Performance, Theory