Deriving algorithms from type inference systems: application to strictness analysis

ABSTRACT

The role of non-standard type inference in static program analysis has been much studied recently. Early work emphasised the efficiency of type inference algorithms and paid little attention to the correctness of the inference system. Recently more powerful inference systems have been investigated but the connection with efficient inference algorithms has been obscured. The contribution of this paper is twofold: first we show how to transform a program logic into an algorithm and, second, we introduce the notion of lazy types and show how to derive an efficient algorithm or strictness analysis.

REFERENCES

• 1: Steffen van Bakel, Complete restrictions of the intersection type discipline, Theoretical Computer Science, v.102 n.1, p.135-163, 3 Aug. 1992 [doi>10.1016/0304-3975(92)90297-S]
• 2: H. Barendregt, M. Coppo, M. Dezani-Ciancaglini, A filter lambda model and the completeness of type assignment, Journal of Symbolic Logic, 48(4), 1983.
• 3: P. N. Benton, Strictness Logic and Polymorphic Invariance, Proceedings of the Second International Symposium on Logical Foundations of Computer Science, p.33-44, July 20-24, 1992
• 4: Tyng-Ruey Chuang , Benjamin Goldberg, A syntactic approach to fixed point computation on finite domains, Proceedings of the 1992 ACM conference on LISP and functional programming, p.109-118, June 22-24, 1992, San Francisco, California, United States
• 5: Chris Clack , Simon L. Peyton Jones, Strictness analysis—a practical approach, Proc. of a conference on Functional programming languages and computer architecture, p.35-49, January 1985, Nancy, France
• 6: Patrick Cousot , Radhia Cousot, Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, p.269-295, August 26-28, 1992
• 7: Marko van Eekelen , Eric Goubault , Chris Hankin , Eric Nöcker, Abstract reduction: towards a theory via abstract interpretation, Term graph rewriting: theory and practice, John Wiley and Sons Ltd., Chichester, UK, 1993
• 8: Alex Ferguson , John Hughes, Fast Abstract Interpretation Using Sequential Algorithms, Proceedings of the Third International Workshop on Static Analysis, p.45-59, September 22-24, 1993
• 9: Chris Hankin , Sebastian Hunt, Approximate fixed points in abstract interpretation, Symposium proceedings on 4th European symposium on programming, p.219-232, January 1992, Rennes, France
• 10: John Joseph Hannan , Dale Miller, Investigating a proof-theoretic meta-language for functional programs, 1990
• 11: J. Hannah and D. Miller, From Operational Semantics to Abstract Machines, Mathematical Structures in Computer Science, 2(4), 1992.
• 12: Fritz Henglein, Efficient type inference for higher-order binding-time analysis, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.448-472, June 1991, Cambridge, Massachusetts, United States
• 13: L. S. Hunt and C. L. Hankin, Fixed Points and Frontiers: A New Perspective, Journal of Functional Programming, 1(1), 1991.
• 14: Thomas P. Jensen, Strictness analysis in logical form, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.352-366, June 1991, Cambridge, Massachusetts, United States
• 15: T. P. Jensen, Abstract Interpretation in Logical Form, PhD thesis, University of London, 1992. Also available as DIKU Technical Report 93/11.
• 16: 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]
• 17: S. L. Peyton Jones and C. Clack, Finding Fixed Points in Abstract Interpretation, in S. Abramsky and C. L. Hankin (eds), Abstract Interpretation of Declarative Languages, Ellis Horwood, 1987.
• 18: Tsung-Min Kuo , Prateek Mishra, Strictness analysis: a new perspective based on type inference, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.260-272, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99390]
• 19: John Launchbury, Strictness and binding-time analyses: two for the price of one, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.80-91, June 24-28, 1991, Toronto, Ontario, Canada
• 20: Allen Leung , Prateek Mishra, Reasoning about simple and exhaustive demand in higher-order lazy languages, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.328-351, June 1991, Cambridge, Massachusetts, United States
• 21: 3. C. Mitchell, Type inference with simple subtypes, 3ournal of Functional Programming, 1(3), 1991.
• 22: Bruno Monsuez, Polymorphic Typing by Abstract Interpretation, Proceedings of the 12th Conference on Foundations of Software Technology and Theoretical Computer Science, p.217-228, December 18-20, 1992
• 23: A. Mycroft, Abstract Interpretation and Optimising Transformations for Applicative Programs, PhD thesis, University of Edinburgh, December 1981.
• 24: Eric Nöcker, Strictness analysis using abstract reduction, Proceedings of the conference on Functional programming languages and computer architecture, p.255-265, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165219]
• 25: P. Wadler, Strictness Analysis on Non-flat Domains, in S. Abramsky and C. L. Hankin (eds), Abstract Interpretation of Declarative Languages, Ellis Horwood, 1987.
• 26: Philip Wadler, Is there a use for linear logic?, Proceedings of the 1991 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.255-273, June 17-19, 1991, New Haven, Connecticut, United States

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Algorithms, Theory