Skip to main content
SpringerLink
Log in

Exact flow analysis

  • Functional Programming II
  • Conference paper
  • First Online:
Static Analysis (SAS 1997)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1302))

Included in the following conference series:

Abstract

We present a type-based flow analysis for simply typed lambda calculus with booleans, data-structures and recursion. The analysis is exact in the following sense: if the analysis predicts a redex, then there exists a reduction sequence (using standard reduction plus context propagation rules) such that this redex will be reduced. The precision is accomplished using intersection typing.

It follows that the analysis is non-elementary recursive — more surprisingly, the analysis is decidable. We argue that the specification of such an analysis provides a good starting point for developing new flow analyses and an important benchmark against which other flow analyses can be compared. Furthermore, we believe that the techniques employed for stating and proving exactness are of independent interest: they provide methods for reasoning about the precision of program analyses.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Banerjee. A modular, polyvariant, and type-based closure analysis. In International Conference on Functional Programming. ACM Press, 1997. To Appear.

    Google Scholar 

  2. H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 1983.

    Google Scholar 

  3. N. Benton. Strictness Analysis of Lazy Functional Programs. PhD thesis, University of Cambridge, December 1992.

    Google Scholar 

  4. M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Functional characters of solvable terms. Zeitschrift für Mathematische Logik and Grundlagen der Mathematik, 27:45–58, 1981.

    Google Scholar 

  5. D. Dussart, F. Henglein, and C. Mossin. Polymorphic recursion and subtype qualifications: Polymorphic binding-time analysis in polynomial time. In Proc. 2nd Int'l Static Analysis Symposium (SAS), volume 983 of LNCS, pages 118–135, 1995.

    Google Scholar 

  6. K.-F. Faxen. Analysing, Transforming and Compiling Lazy Functional Programs. PhD thesis, Royal Institute of Technology, Sweden, 1997.

    Google Scholar 

  7. C. Gomard. Higher order partial evaluation-hope for the lambda calculus. Master's thesis, DIKU, University of Copenhagen, Denmark, September 1989.

    Google Scholar 

  8. N. Heintze. Control-flow analysis and type systems. In Symposium on Static Analysis (SAS), volume 983 of LNCS, pages 189–206, Glasgow, 1995.

    Google Scholar 

  9. N. Heintze and D. McAllester. Linear-time subtransitive control flow analysis. In Programming Language Design and Implementation (PLDI), 1997.

    Google Scholar 

  10. F. Henglein. Dynamic typing: Syntax and proof theory. Science of Computer Programming (SCP), 22(3):197–230, 1994.

    Google Scholar 

  11. F. Henglein and J. Jørgensen. Formally optimal boxing. In Proc. 21st ACM Symp. on Principles of Programming Languages (POPL), Portland, Oregon. ACM, 1994.

    Google Scholar 

  12. F. Henglein and C. Mossin. Polymorphic binding-time analysis. In D. Sannella, editor, Proceedings of European Symposium on Programming, volume 788 of Lecture Notes in Computer Science, pages 287–301. Springer-Verlag, Apr. 1994.

    Google Scholar 

  13. S. Jaganathan and S. Weeks. A unified treatment of flow analysis in higher-order languages. In POPL'95, pages 393-407. ACM Press, 1995.

    Google Scholar 

  14. T. Jensen. Abstract Interpretation in Logical Form. PhD thesis, Imperial College, Univ. of London, November 1992. Available as DIKU Report 93/11.

    Google Scholar 

  15. J. Jørgensen. A Calculus for Boxing Analysis of Polymorphically Typed Languages. PhD thesis, DIKU, University of Copenhagen, October 1995.

    Google Scholar 

  16. T. Kuo and P. Mishra. On strictness and its analysis. In Proc. 14th Annual ACM Symposium on Principles of Programming Languages, pages 144–155, Jan. 1987.

    Google Scholar 

  17. T. Kuo and P. Mishra. Strictness analysis: A new perspective based on type inference. In Proc. Functional Programming Languages and Computer Architecture (FPCA), London, England, pages 260–272. ACM Press, Sept. 1989.

    Google Scholar 

  18. X. Leroy. Unboxed objects and polymorphic typing. In Proc. 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programmin gLanguages (POPL), Albuquerque, New Mexico, pages 177–188. ACM Press, Jan. 1992.

    Google Scholar 

  19. J. M. Lucassen and D. K. Gifford. Polymorphic effect systems. In Principles of Programming Languages (POPL). ACM, 1988.

    Google Scholar 

  20. C. Mossin. Exact flow analysis. Technical report, DIKU, 1997.

    Google Scholar 

  21. C. Mossin. Flow Analysis of Typed Higher-Order Programs. PhD thesis, DIKU, University of Copenhagen, January 1997.

    Google Scholar 

  22. F. Nielson and H. R. Nielson. Infinitary control flow analysis: a collecting semantics for closure analysis. In 24th Symposium on Principles of Programming Languages, pages 332–345, 1997.

    Google Scholar 

  23. H. R. Nielson and F. Nielson. Automatic binding time analysis for a typed lambda-calculus. In Fifteenth ACM Symposium on Principles of Programming Languages, pages 98–106. ACM Press, January 1988. Extended Abstract.

    Google Scholar 

  24. J. Palsberg. Global program analysis in constraint form. In 19th International Colloquium on Trees in Algebra and Programming (CAAP'94), volume 787 of LNCS, pages 276–290, 1994.

    Google Scholar 

  25. J. Palsberg and P. O'Keefe. A type system equivalent to flow analysis. In Principles of Programming Languages, 1995.

    Google Scholar 

  26. P. Sestoft. Analysis and Efficient Implementation of Functional Languages. PhD thesis, DIKU, University of Copenhagen, Oct. 1991.

    Google Scholar 

  27. O. Shivers. Control-Flow Analysis of Higher-Order Languages. PhD thesis, Carnegie Mellon University, May 1991. CMU-CS-91-145.

    Google Scholar 

  28. K. L. Solberg. Strictness and totality analysis. In Symposium on Static Analysis, pages 408–422, 1994.

    Google Scholar 

  29. K. L. Solberg. Strictness and totality analysis with conjunction. In TAPSOFT, pages 501–515, 1995.

    Google Scholar 

  30. R. Statman. The typed λ-calculus is not elementary recursive. Theoretical Computer Science, 9(1):73–81, Juli 1979.

    Google Scholar 

  31. J.-P. Talpin and P. Jouvelot. The type and effect discipline. Information and Computation, 111:245–296, 1994.

    Google Scholar 

  32. D. Wright. A new technique for strictness analysis. In Proc. Int'l J. Conf. on Theory and Practice of Software Development (TAPSOFT), April 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DIKU, Universitetsparken 1, DK-2100, Copenhagen Ø, Denmark

    Christian Mossin

Authors
  1. Christian Mossin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Pascal Van Hentenryck

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mossin, C. (1997). Exact flow analysis. In: Van Hentenryck, P. (eds) Static Analysis. SAS 1997. Lecture Notes in Computer Science, vol 1302. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0032746

Download citation

  • DOI: https://doi.org/10.1007/BFb0032746

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63468-3

  • Online ISBN: 978-3-540-69576-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation