Implementation of the typed call-by-value λ-calculus using a stack of regions

ABSTRACT

We present a translation scheme for the polymorphically typed call-by-value &lgr;-calculus. All runtime values, including function closures, are put into regions. The store consists of a stack of regions. Region inference and effect inference are used to infer where regions can be allocated and de-allocated. Recursive functions are handled using a limited form of polymorphic recursion. The translation is proved correct with respect to a store semantics, which models as a region-based run-time system. Experimental results suggest that regions tend to be small, that region allocation is frequent and that overall memory demands are usually modest, even without garbage collection.

REFERENCES

• 1: A. J. Kfoury , J. Tiuryn , P. Urzyczyn, Type reconstruction in the presence of polymorphic recursion, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.290-311, April 1993 [doi>10.1145/169701.169687]
• 2: Andrew W. Appel, Compiling with continuations, Cambridge University Press, New York, NY, 1992
• 3: Henry G. Baker, Unify and conquer, Proceedings of the 1990 ACM conference on LISP and functional programming, p.218-226, June 27-29, 1990, Nice, France [doi>10.1145/91556.91652]
• 4: Henry G. Baker, Jr., List processing in real time on a serial computer, Communications of the ACM, v.21 n.4, p.280-294, April 1978 [doi>10.1145/359460.359470]
• 5: D. R. Chase, Safety consideration for storage allocation optimizations, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.1-10, June 20-24, 1988, Atlanta, Georgia, United States
• 6: J. M. Lucassen D. K. Gifford, P. Jouvelot and M.A. Sheldon. FX-87 Reference Manual. Technical Report MIT/LCS/TR-407, MIT Laboratory for Computer Science, Sept 1987.
• 7: Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
• 8: Jo~lle Despeyroux. Proof of translation in natural semantics. In Proc. of the 1st Symp. on Logic in Computer Science, IEEE, Cambridge, USA, 1986.
• 9: Rosen Saul, Programming Systems and Languages., McGraw Hill Text, 1967
• 10: Michael Georgeff, Transformations and reduction strategies for typed lambda expressions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.4, p.603-631, Oct. 1984 [doi>10.1145/1780.1803]
• 11: Barry Hayes, Using key object opportunism to collect old objects, ACM SIGPLAN Notices, v.26 n.11, p.33-46, Nov. 1991
• 12: Fritz Henglein, Type inference with polymorphic recursion, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.253-289, April 1993 [doi>10.1145/169701.169692]
• 13: Paul Hudak, A semantic model of reference counting and its abstraction (detailed summary), Proceedings of the 1986 ACM conference on LISP and functional programming, p.351-363, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319876]
• 14: Pierre Jouvelot , David Gifford, Algebraic reconstruction of types and effects, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.303-310, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99623]
• 15: Katsuro Inoue , Hiroyuki Seki , Hikaru Yagi, Analysis of functional programs to detect run-time garbage cells, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.4, p.555-578, Oct. 1988 [doi>10.1145/48022.48025]
• 16: Åke Wikström, Functional programming using standard ML, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1987
• 17: A. J. Kfoury , J. Tiuryn , P. Urzyczyn, The undecidability of the semi-unification problem, Proceedings of the twenty-second annual ACM symposium on Theory of computing, p.468-476, May 13-17, 1990, Baltimore, Maryland, United States [doi>10.1145/100216.100279]
• 18: Donald E. Knuth. Fundamental Algorithms. Volume 1 of The Art of Computer Programming, Addison-Wesley, 1972.
• 19: Henry Lieberman , Carl Hewitt, A real-time garbage collector based on the lifetimes of objects, Communications of the ACM, v.26 n.6, p.419-429, June 1983 [doi>10.1145/358141.358147]
• 20: J. M. Lucassen. Types and Effects, towards the integration of functional and imperative programming. PhD thesis, MIT Laboratory for Computer Science, 1987. MIT/LCS/TR-408.
• 21: J. M. Lucassen , D. K. Gifford, Polymorphic effect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-57, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73564]
• 22: R. Milner. A theory of type polymorphism in programming. J. Computer and System Sciences, 17:348-375, 1978.
• 23: Robin Milner , Mads Tofte, Co-induction in relational semantics, Theoretical Computer Science, v.87 n.1, p.209-220, Sept. 16, 1991 [doi>10.1016/0304-3975(91)90033-X]
• 24: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 25: F. Lockwood Morris, Advice on structuring compilers and proving them correct, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.144-152, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512941]
• 26: Alan Mycroft, Polymorphic Type Schemes and Recursive Definitions, Proceedings of the 6th Colloquium on International Symposium on Programming, p.217-228, April 17-19, 1984
• 27: Laurence C. Paulson, ML for the working programmer, Cambridge University Press, New York, NY, 1991
• 28: C. Ruggieri , T. P. Murtagh, Lifetime analysis of dynamically allocated objects, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.285-293, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73585]
• 29: Jean-Pierre Talpin. Theoretical and practical aspects of type and effect inference. Doctoral Dissertation. May 1993. Also available as Research Report EMP/CRI/A-236, Ecole des Mines de Paris.
• 30: Jean-Pierre Talpin and Pierre Jouvelot. Polymorphic type, region and effect inference. Journal of Functional Programming, 2(3), 1992.
• 31: Mads Tofte and Jean-Pierre Talpin. A Theory of Stack Allocation in Polymorphicalty Typed Languages. Technical Report DIKU-report 93/15, Department of Computer Science, University of Copenhagen, 1993.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Languages, Theory, Verification