Skip to main content
SpringerLink
Log in

Strictness and totality analysis

  • Conference paper
  • First Online:
Book cover Static Analysis (SAS 1994)

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

Included in the following conference series:

Abstract

We define a novel inference system for strictness and totality analysis for the simplytyped lazy lambda-calculus with constants and fixpoints. Strictness information identifies those terms that definitely denote bottom (i.e. do not evaluate to WHNF) whereas totality information identifies those terms that definitely do not denote bottom (i.e. do evaluate to WHNF). The analysis is presented as an annotated type system allowing conjunctions only at “top-level”. We give examples of its use and prove the correctness with respect to a natural-style operational semantics.

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. Samson Abramsky. Abstract interpretation, logical relations and Kan extensions. Journal of Logic and Computation, 1(1):5–39, 1990.

    Google Scholar 

  2. Nick Benton. Strictness Analysis of Functional Programs. PhD thesis, University of Cambridge, 1993. Available as Technical Report No. 309.

    Google Scholar 

  3. Stefano Berardi. “Pruning” simply typed λ-terms. Technical report, Turin University, 1993.

    Google Scholar 

  4. Geoffrey L. Burn, Chris Hankin, and Samson Abramsky. Strictness analysis for higher-order functions. Science of Computer Programming, 7:249–278, 1986.

    Article  Google Scholar 

  5. Philippa Gardner. Discovering needed reductions using type theory. In Proceeding of TACS'94, 1994.

    Google Scholar 

  6. Chris Hankin and Daniel Le Métayer. Deriving algorithms from type inference systems: Application to strictness analysis. In Proceedings of POPL'94, pages 202–212, 1994.

    Google Scholar 

  7. Chris Hankin, and Daniel Le Métayer. Lazy type inference for the strictness analysis of lists. In Proceedings of ESOP'94, LNCS 788, pages 257–271, 1994.

    Google Scholar 

  8. Thomas P. Jensen. Strictness analysis in logical form. In Proceedings FPCA'91, LNCS 523, pages 352–366, 1991.

    Google Scholar 

  9. Thomas P. Jensen. Disjunctive strictness analysis. In Proceedings LICS' 92, pages 174–185, 1992.

    Google Scholar 

  10. Tsung-Min Kuo and Prateek Mishra. Strictness analysis: A new perspective based on type inference. In Proceedings of FPCA'89, pages 260–272. ACM Press, 1989.

    Google Scholar 

  11. Alan Mycroft. The theory and practice of transforming call-by-need into call-by-value. In Proceeding of the 4th International Symposium on Programming, LNCS 83, pages 269–281, 1980.

    Google Scholar 

  12. Alan Mycroft. Abstract Interpretation and Optimising Transformation for Applicative programs. PhD thesis, University of Edinburgh, Scotland, 1981.

    Google Scholar 

  13. Alan Mycroft, and Flemming Nielson. Strong abstract interpretation using power domain (extended abstract). In Proceedings of ICALP'83, LNCS 154, pages 536–547, 1983.

    Google Scholar 

  14. Flemming Nielson, Hanne Riis Nielson. Termination Analysis. Manuscript, Aarhus University, 1994.

    Google Scholar 

  15. David Sands. Complexity Analysis for a Lazy Higher-Order Language. In Proceedings of ESOP'90, LNCS 432, pages 361–376, 1990.

    Google Scholar 

  16. Kirsten Lackner Solberg. Strictness and totality analysis. Forthcoming report, Odense University, Denmark, 1994.

    Google Scholar 

  17. Jean-Pierre Talpin, and Pierre Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3):162–173, 1992.

    Google Scholar 

  18. Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. In Proceedings of LICS'92, 1992.

    Google Scholar 

  19. Mads Tofte and Jean-Pierre Talpin. Data region inference for polymorphic functional languages. In Proceedings of POPL'94, pages 188–201, 1994.

    Google Scholar 

  20. D. A. Turner. Miranda: A non-strict functional language with polymorphic types. In Proceeding of FPCA'85, LNCS 201, pages 1–16, 1985.

    Google Scholar 

  21. Phil Wadler. Strictness analysis on non-flat domains by abstract interpretation over finite domains. In S. Abramsky and C. Hankin (eds.), editors, Abstract Interpretation of Declarative Languages, pages 266–275. Ellis Horwood, 1987.

    Google Scholar 

  22. Phil Wadler, John Hughes. Projections for strictness analysis. In Proceedings of FPCA'87, LNCS 274, 1987.

    Google Scholar 

  23. David A. Wright. A new technique for strictness analysis. In Proceedings of TAPSOFT'91, LNCS 494, pages 260–272, 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Math. and Computer Science, Odense University, Denmark

    Kirsten Lackner Solberg

  2. Computer Science Dept., Aarhus University, Denmark

    Kirsten Lackner Solberg, Hanne Riis Nielson & Flemming Nielson

Authors
  1. Kirsten Lackner Solberg
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hanne Riis Nielson
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Flemming Nielson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Baudouin Le Charlier

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Solberg, K.L., Nielson, H.R., Nielson, F. (1994). Strictness and totality analysis. In: Le Charlier, B. (eds) Static Analysis. SAS 1994. Lecture Notes in Computer Science, vol 864. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58485-4_55

Download citation

  • DOI: https://doi.org/10.1007/3-540-58485-4_55

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58485-8

  • Online ISBN: 978-3-540-49005-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation