A Type System for Bounded Space and Functional In-Place Update—Extended Abstract

  • Martin Hofmann
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1782)


We show how linear typing can be used to obtain functional programs which modify heap-allocated data structures in place.

We present this both as a “design pattern” for writing C-code in a functional style and as a compilation process from linearly typed first-order functional programs into malloc()-free C code.

The main technical result is the correctness of this compilation.

The crucial innovation over previous linear typing schemes consists of the introduction of a resource type ◊ which controls the number of constructor symbols such as cons in recursive definitions and ensures linear space while restricting expressive power surprisingly little.

While the space efficiency brought about by the new typing scheme and the compilation into C can also be realised by with state-of-the-art optimising compilers for functional languages such as Ocaml [15], the present method provides guaranteed bounds on heap space which will be of use for applications such as languages for embedded systems or ‘proof carrying code’ [18].


Type System Garbage Collection Linear Logic Resource Type Space Usage 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Samson Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111:3–57, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Henry Baker. Lively Linear LISP—Look Ma, No Garbage. ACM Sigplan Notices, 27(8):89–98, 1992.CrossRefGoogle Scholar
  3. 3.
    Henry Baker. A Linear Logic Quicksort. ACM Sigplan Notices, 29(2):13–18, 1994.CrossRefGoogle Scholar
  4. 4.
    E. Barendsen and S. Smetsers. Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science, 6:579–612, 1996.zbMATHMathSciNetGoogle Scholar
  5. 5.
    Vuokko-Helena Caseiro. Equations for Defining Poly-time Functions. PhD thesis, University of Oslo, 1997. Available by ftp from
  6. 6.
    J. Chirimar, C. Gunter, and J. Riecke. Reference counting as a computational interpretation of linear logic. Journal of Functional Programming, 6(2), 1995.Google Scholar
  7. 7.
    K. Crary and S. Weirich. Resource bound certification. In Proc. 27th Symp. Principles of Prog. Lang. (POPL). ACM, 2000. to appear.Google Scholar
  8. 8.
    J.-Y. Girard, A. Scedrov, and P. Scott. Bounded linear logic. Theoretical Computer Science, 97(1):1–66, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Martin Hofmann. Linear types and non size-increasing polynomial time computation. In Logic in Computer Science (LICS). IEEE, Computer Society Press, 1999. to appear.Google Scholar
  10. 10.
    Sören Holmström. A linear functional language. In Proceedings of the Workshop on Implemenation of Lazy Functional Languages. Chalmers University, Göteborg, Programming Methodology Group, Report 53, 1988.Google Scholar
  11. 11.
    Paul Hudak and Chih-Ping Chen. Rolling your own mutable adt — a connection between linear types and monads. In Proc. Symp. POPL’ 97, ACM, 1997.Google Scholar
  12. 12.
    J. Hughes and L. Pareto. Recursion and dynamic data structures in bounded space: towards embedded ml programming. In Proc. International Conference on Functional Programming. Paris, September’ 99., 1999. to appear.Google Scholar
  13. 13.
    Kelley and Pohl. A book on C, third edition. Benjamin/Cummings, 1995.Google Scholar
  14. 14.
    Yves Lafont. The linear abstract machine. Theoretical Computer Science, 59:157–180, 1988.CrossRefzbMATHMathSciNetGoogle Scholar
  15. 15.
    Xavier Leroy. The Objective Caml System, documentation and user’s guide. Release 2.02., 1999.
  16. 16.
    P. Lincoln and J. Mitchell. Operational aspects of linear lambda calculus. In Proc. LICS 1992, IEEE, 1992.Google Scholar
  17. 17.
    Alan Mycroft. Abstract interpretation and optimising transformations for applicative programs. PhD thesis, Univ. Edinburgh, 1981.Google Scholar
  18. 18.
    George Necula. Proof-carrying code. In Proc. 24th Symp. Principles of Prog. Lang. (POPL). ACM, 1997. to appear.Google Scholar
  19. 19.
    M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132(2):109–176, 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Mads Tofte and Lars Birkedal. Region inference algorithm. ACM Transactions on Programming Languages and Systems, 20(5):724–767, 1998.CrossRefGoogle Scholar
  21. 21.
    D. Turner and P. Wadler. Operational interpretations of linear logic. Theoretical Computer Science, 1999. to appear.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Martin Hofmann
    • 1
  1. 1.LFCS EdinburghEdinburghUK

Personalised recommendations