Skip to main content
SpringerLink
Log in

Stack-based Typed Assembly Language

  • Conference paper
  • First Online:
Types in Compilation (TIC 1998)

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

Included in the following conference series:

Abstract

In previous work, we presented a Typed Assembly Language (TAL). TAL is sufficiently expressive to serve as a target language for compilers of high-level languages such as ML. This work assumed such a compiler would perform a continuation-passing style transform and eliminate the control stack by heap-allocating activation records. However, most compilers are based on stack allocation. This paper presents STAL, an extension of TAL with stack constructs and stack types to support the stack allocation style. We show that STAL is sufficiently expressive to support languages such as Java, Pascal, and ML; constructs such as exceptions and displays; and optimizations such as tail call elimination and callee-saves registers. This paper also formalizes the typing connection between CPS-based compilation and stack-based compilation and illustrates how STAL can formally model calling conventions by specifying them as formal translations of source function types to STAL types.

This material is based on work supported in part by the AFOSR grant F49620-97-1-0013, ARPA/RADC grant F30602-96-1-0317, ARPA/AF grant F30602-95-1-0047, and AASERT grant N00014-95-1-0985. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the authors and do not reflect the views of these agencies.

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. Andrew W. Appel and Trevor Jim. Continuation-passing, closure-passing style. In Sixteenth ACM Symposium on Principles of Programming Languages, pages 293–302, Austin, January 1989.

    Google Scholar 

  2. Andrew W. Appel and David B. MacQueen. Standard ML of New Jersey. In Martin Wirsing, editor, Third International Symposium on Programming Language Implementation and Logic Programming, pages 1–13, New York, August 1991. Springer-Verlag. Volume 528 of Lecture Notes in Computer Science.

    Google Scholar 

  3. Andrew W. Appel. Compiling with Continuations. Cambridge University Press, 1992.

    Google Scholar 

  4. Andrew Appel and Zhong Shao. Callee-saves registers in continuation-passing style. Lisp and Symbolic Computation, 5: 189–219, 1992.

    Article  Google Scholar 

  5. Andrew Appel and Zhong Shao. An empirical and analytic study of stack vs. heap cost for languages with clsoures. Journal of Functional Programming, 1(1), January 1993.

    Google Scholar 

  6. Mark Bailey and Jack Davidson. A formal model of procedure calling conventions. In Twenty-Second ACM Symposium on Principles of Programming Languages, pages 298–310, San Francisco, January 1995.

    Google Scholar 

  7. Lars Birkedal, Nick Rothwell, Mads Tofte, and David N. Turner. The ML Kit (version 1). Technical Report 93/14, Department of Computer Science, University of Copenhagen, 1993.

    Google Scholar 

  8. Lars Birkedal, Mads Tofte, and Magnus Vejlstrup. From region inference to von Neumann machines via region representation inference. In Twenty-Third ACM Symposium on Principles of Programming Languages, pages 171–183, St. Petersburg, January 1996.

    Google Scholar 

  9. Val Breazu-Tannen, Thierry Coquand, Carl A. Gunter, and Andre Scedrov. Inheritance as implicit coercion. Information and Computation, 93: 172–221, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  10. Karl Crary. KML Reference Manual. Department of Computer Science, Cornell University, 1996.

    Google Scholar 

  11. Karl Crary. Foundations for the implementation of higher-order subtyping. In ACM SIGPLAN International Conference on Functional Programming, pages 125–135, Amsterdam, June 1997.

    Google Scholar 

  12. Allyn Dimock, Robert Muller, Franklyn Turbak, and J. B. Wells. Strongly typed flow-directed reprsentation transformations. In ACM SIGPLAN International Conference on Functional Programming, pages 11–24, Amsterdam, June 1997.

    Google Scholar 

  13. Amer Diwan, David Tarditi, and Eliot Moss. Memory subsystem performance of programs using copying garbage collection. In Twenty-First ACM Symposium on Principles of Programming Languages, pages 1–14, January 1994.

    Google Scholar 

  14. Amer Diwan, David Tarditi, and Eliot Moss. Memory system performance of programs with intensive heap allocation. ACM Transactions on Computer Systems, 13(3): 244–273, August 1995.

    Article  Google Scholar 

  15. Robert Hieb, R. Kent Dybvig, and Carl Bruggeman. Representing control in the presence of first-class continuations. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 66–77, June 1990. Published as SIGPLAN Notices, 25(6).

    Google Scholar 

  16. Intel Corporation. Intel Architecture Optimization Manual. Intel Corporation, P.O. Box 7641, Mt. Prospect, IL, 60056-7641, 1997.

    Google Scholar 

  17. David Kranz, R. Kelsey, J. Rees, P. R. Hudak, J. Philbin, and N. Adams. ORBIT: An optimizing compiler for Scheme. In Proceedings of the ACM SIGPLAN ’86 Symposium on Compiler Construction, pages 219–233, June 1986.

    Google Scholar 

  18. P. J. Landin. The mechanical evaluation of expressions. Computer J., 6(4): 308–20, 1964.

    MATH  Google Scholar 

  19. Xavier Leroy. Unboxed objects and polymorphic typing. In Nineteenth ACM Symposium on Principles of Programming Languages, pages 177–188, Albuquerque, January 1992.

    Google Scholar 

  20. Tim Lindholm and Frank Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1996.

    Google Scholar 

  21. Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. In Twenty-Third ACM Symposium on Principles of Programming Languages, pages 271–283, St. Petersburg, January 1996.

    Google Scholar 

  22. Gregory Morrisett. Compiling with Types. PhD thesis, Carnegie Mellon University, 1995. Published as CMU Technical Report CMU-CS-95-226.

    Google Scholar 

  23. Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. In Twenty-Fifth ACM Symposium on Principles of Programming Languages, San Diego, January 1998. Extended version published as Cornell University technical report TR97-1651, November 1997.

    Google Scholar 

  24. G. Morrisett, D. Tarditi, P. Cheng, C. Stone, R. Harper, and P. Lee. The TIL/ML compiler: Performance and safety through types. In Workshop on Compiler Support for Systems Software, Tucson, February 1996.

    Google Scholar 

  25. Simon L. Peyton Jones, Cordelia V. Hall, Kevin Hammond, Will Partain, and Philip Wadler. The Glasgow Haskell compiler: a technical overview. In Proc. UK Joint Framework for Information Technology (JFIT) Technical Conference, July 1993.

    Google Scholar 

  26. John C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing ’83, pages 513–523. North-Holland, 1983. Proceedings of the IFIP 9th World Computer Congress.

    Google Scholar 

  27. John Reynolds. Using functor categories to generate intermediate code. In Twenty-Second ACM Symposium on Principles of Programming Languages, pages 25–36, San Francisco, January 1995.

    Google Scholar 

  28. Zhong Shao. Flexible representation analysis. In ACM SIGPLAN International Conference on Functional Programming, pages 85–98, Amsterdam, June 1997.

    Google Scholar 

  29. Z. Shao. An overview of the FLINT/ML compiler. In Workshop on Types in Compilation, Amsterdam, June 1997. ACM SIGPLAN. Published as Boston College Computer Science Dept. Technical Report BCCS-97-03.

    Google Scholar 

  30. Raymie Stata and Martín Abadi. A type system for Java bytecode subroutines. In Twenty-Fifth A CM Symposium on Principles of Programming Languages, San Diego, January 1998.

    Google Scholar 

  31. Guy L. Steele Jr. Rabbit: A compiler for Scheme. Master’s thesis, MIT, 1978.

    Google Scholar 

  32. D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: A type-directed optimizing compiler for ML. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 181–192, Philadelphia, May 1996.

    Google Scholar 

  33. Mads Tofte and Jean-Pierre Talpin. Implementation of the typed call-by-value λ-calculus using a stack of regions. In Twenty-First ACM Symposium on Principles of Programming Languages, pages 188–201, January 1994.

    Google Scholar 

  34. Mitchell Wand. Continuation-based multiprocessing. In Proceedings of the 1980 LISP Conference, pages 19–28, August 1980.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Cornell University, UK

    Greg Morrisett, Karl Crary, Neal Glew & David Walker

Authors
  1. Greg Morrisett
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Karl Crary
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Neal Glew
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. David Walker
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Xavier Leroy Atsushi Ohori

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Morrisett, G., Crary, K., Glew, N., Walker, D. (1998). Stack-based Typed Assembly Language. In: Leroy, X., Ohori, A. (eds) Types in Compilation. TIC 1998. Lecture Notes in Computer Science, vol 1473. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055511

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64925-0

  • Online ISBN: 978-3-540-68308-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation