Abstract
On the basis of an A-normal form intermediate language we formally specify resource allocation in a compiler for a strict functional language. Here, resource is to be understood in the most general sense: registers, temporaries, data representations, etc. All these should be (and can be, but have never been) specified formally. Our approach employs a non-standard annotated type system for the formalization. Although A-normal form turns out not to be the ideal vehicle for this investigation, we can prove some basic properties using the formalization.
Preview
Unable to display preview. Download preview PDF.
References
Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers Principles, Techniques, and Tools. Addison-Wesley, 1986.
Andrew W. Appel. Compiling with Continuations. Cambridge University Press, 1992.
Andrew W. Appel and Trevor Jim. Continuation-passing, closure-passing style. In POPL1989 [16], pages 293–302.
Lars Birkedal, Mads Tofte, and Magnus Vejlstrup. From region inference to von Neumann machines via region representation inference. In Proc. 23rd Annual ACM Symposium on Principles of Programming Languages, pages 171–183, St. Petersburg, Fla., January 1996. ACM Press.
Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. In Proc. of the ACM SIGPLAN ’93 Conference on Programming Language Design and Implementation, pages 237–247, Albuquerque, New Mexico, June 1993.
Christopher W. Fraser and David R. Hanson. A Retargetable C Compiler: Design and Implementation. Benjamin/Cummings, 1995.
David K. Gifford and John M. Lucassen. Integrating functional and imperative programming. In Proceedings of the 1986 ACM conference on Lisp and Functional Programming, pages 28–38, 1986.
Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50: 1–102, 1987.
John Hatcliff and Olivier Danvy. A generic account of continuation-passing styles. In POPL1994 [17], pages 458–471.
Fritz Henglein and Jesper Jørgensen. Formally optimal boxing. In POPL1994 [17], pages 213–226.
Pierre Jouvelot and David K. Gifford. Algebraic reconstruction of types and effects. In Proc. 18th Annual ACM Symposium on Principles of Programming Languages, pages 303–310, Orlando, Florida, January 1991. ACM Press.
Richard Kelsey and Paul Hudak. Realistic compilation by program transformation. In POPL1989 [16], pages 281–292.
D. Kranz, R. Kelsey, J. Rees, P. Hudak, J. Philbin, and N. Adams. ORBIT: An optimizing compiler for Scheme. SIGPLAN Notices, 21(7): 219–233, July 1986. Proc. Sigplan ’86 Symp. on Compiler Construction.
Peter Lee. The origin of nqCPS. Email message, March 1998.
Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From system F to typed assembly language. In Luca Cardelli, editor, Proc. 25th Annual ACM Symposium on Principles of Programming Languages, San Diego, CA, USA, January 1998. ACM Press.
16th Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, January 1989. ACM Press.
Proc. 21st Annual ACM Symposium on Principles of Programming Languages, Portland, OG, January 1994. ACM Press.
Zhong Shao. Flexible representation analysis. In Mads Tofte, editor, Proc. International Conference on Functional Programming 1997, pages 85–98, Amsterdam, The Netherlands, June 1997. ACM Press, New York.
Zhong Shao and Andrew W. Appel. A type-based compiler for Standard ML. In Proc. of the ACM SIGPLAN ’95 Conference on Programming Language Design and Implementation, La Jolla, CA, USA, June 1995. ACM Press.
Paul Steckler and Mitchell Wand. Lightweight closure conversion. ACM Transactions on Programming Languages and Systems, 19(1): 48–86, January 1997.
Guy L. Steele. Rabbit: a compiler for Scheme. Technical Report AI-TR-474, MIT, Cambridge, MA, 1978.
Peter Thiemann. Polymorphic typing and unboxed values revisited. In Simon Peyton Jones, editor, Proc. Functional Programming Languages and Computer Architecture 1995, pages 24–35, La Jolla, CA, June 1995. ACM Press, New York.
Philip Wadler. Is there a use for linear logic? In Paul Hudak and Neil D. Jones, editors, Proc. ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation PEPM ’91, pages 255–273, New Haven, CT, June 1991. ACM. SIGPLAN Notices 26(9).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Thiemann, P. (1998). Formalizing resource allocation in a compiler. 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/BFb0055518
Download citation
DOI: https://doi.org/10.1007/BFb0055518
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