[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

A type-based analysis for stack allocation in functional languages

  • Contributed Papers
  • Conference paper
  • First Online:
Static Analysis (SAS 1995)

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

Included in the following conference series:

Abstract

We consider the problem of detecting when bindings for variables in a higher-order, call-by-value functional language can be allocated on a stack. We use an annotated type system to infer information about the occurrence and extent of variables in a simple higher-order functional language and combine this system with a translation to an annotated language which explicitly indicates when stack allocation can be performed. This technique supports both stack and heap allocation of variable bindings. Only the stack allocated bindings need follow the protocol for stacks: their extent must coincide with their scope. Heap allocated bindings can have any extent and their allocation has no impact on the stack allocated ones. The type system uses a simple notion of annotated types in which types encode not only the typical simple type information, but also information about the use of variables. We demonstrate the use of our analysis by defining both an operational semantics and an abstract machine which utilize both a stack and an environment for variable allocation.

Supported in part by an NSF CAREER award

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.

Similar content being viewed by others

References

  1. M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, October 1991.

    Google Scholar 

  2. Torben Amtoft. Minimal thunkification. In Patrick Courot, Moreno Falaschi, Gilberto Filè, and Antoine Rauzy, editors, Third International Workshop on Static Analysis, volume 724 of Lecture Notes in Computer Science, pages 218–229. Springer-Verlag, 1993.

    Google Scholar 

  3. Anindya Banerjee and David A. Schmidt. Stackability in the simply-typed call-by-value lambda calculus. In Baudoin Le Charlier, editor, First International Static Analysis Symposium, volume 864 of Lecture Notes in Computer Science, pages 131–146. Springer-Verlag, 1994.

    Google Scholar 

  4. Luis Damas. Type Assignment in Programming Language. PhD thesis, University of Edinburgh, 1985. Available as CST-33-85.

    Google Scholar 

  5. Benjamin Goldberg and Young Gil Park. Higher order esape analysis: Optimizing stack allocation in functional program implementations. In Neil Jones, editor, Proceedings of the Third European Symposium on Programming, volume 432 of Lecture Notes in Computer Science, pages 152–160. Springer-Verlag, 1990.

    Google Scholar 

  6. John Hannan. Type systems for closure conversions. In Hanne Riis Nielson and Kirsten Lackner Solberg, editors, Participants' Proceedings of the Workshop on Types for Program Analysis, pages 48–62. Aarhus University, DAIMI PB-493, May 1995.

    Google Scholar 

  7. John Hannan and Dale Miller. From operational semantics to abstract machines. Mathematical Structures in Computer Science, 2(4):415–459, 1992. Appears in a special issue devoted to the 1990 ACM Conference on Lisp and Functional Programming.

    Google Scholar 

  8. John Hannan and Frank Pfenning. Compiler verification in LF. In Andre Scedrov, editor, Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pages 407–418. IEEE Computer Society Press, 1992.

    Google Scholar 

  9. Fritz Henglein. Iterative fixed point computation for type-based stritness analysis. In Baudouin Le Charlier, editor, First International Static Analysis Symposium, volume 864 of Lecture Notes in Computer Science, pages 395–407. Springer-Verlag, 1994.

    Google Scholar 

  10. Peter Sestoft. Analysis and Efficient Implementation of Functional Programs. Rapport nr 92/6, DIKU, Copenhagen, October 1991.

    Google Scholar 

  11. Mads Tofte. Operational Semantics and Polymorphic Type Inference. PhD thesis, University of Edinburgh, 1987.

    Google Scholar 

  12. Mads Tofte and Jean-Pierre Talpin. Implementation of the typed call-by-value λ-calculus using a stack of regions. In Conf. Rec. 21st ACM Symposium on Principles of Programming Languages, pages 188–201,1994.

    Google Scholar 

  13. Mitchell Wand and Paul Steckler. Selective and lightweight closure conversion. In Conf. Rec. 21st ACM Symposium on Principles of Programming Languages, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science and Engineering, The Pennsylvania State University, 16802, University Park, PA, USA

    John Hannan

Authors
  1. John Hannan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Alan Mycroft

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hannan, J. (1995). A type-based analysis for stack allocation in functional languages. In: Mycroft, A. (eds) Static Analysis. SAS 1995. Lecture Notes in Computer Science, vol 983. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60360-3_39

Download citation

  • DOI: https://doi.org/10.1007/3-540-60360-3_39

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-45050-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation