Abstract
The type-and-effects system of the Tofte-Talpin region calculus makes it possible to safely reclaim objects without a garbage collector. However, it requires that regions have last-in-first-out (LIFO) lifetimes following the block structure of the language. We introduce λrgnUL, a core calculus that is powerful enough to encode Tofte-Talpin-like languages, and that eliminates the LIFO restriction. The target language has an extremely simple, substructural type system. To prove the power of the language, we sketch how Tofte-Talpin-style regions, as well as the first-class dynamic regions and unique pointers of the Cyclone programming language can be encoded in λrgnUL.
Chapter PDF
References
Cyclone, version 0.9. (2005), http://www.eecs.harvard.edu/~greg/cyclone/
Tofte, M., Talpin, J.P.: Region-based memory management. Information and Computation 132(2), 109–176 (1997)
Hicks, M., Morrisett, G., Grossman, D., Jim, T.: Experience with safe manual memory-management in Cyclone. In: Proc. International Symposium on Memory Management, pp. 73–84 (2004)
Fluet, M., Wang, D.: Implementation and performance evaluation of a safe runtime system in Cyclone. In: Proc. SPACE Workshop (2004)
Grossman, D., Morrisett, G., Jim, T., Hicks, M., Wang, Y., Cheney, J.: Regionbased memory management in Cyclone. In: Proc. Programming Language Design and Implementation, pp. 282–293 (2002)
Fluet, M., Morrisett, G.: Monadic regions. In: Proc. International Conference on Functional Programming, pp. 103–114 (2004)
Launchbury, J., Peyton Jones, S.: State in Haskell. Lisp and Symbolic Computation 8(4), 293–341 (1995)
Ahmed, A., Fluet, M., Morrisett, G.: A step-indexed model of substructural state. In: Proc. International Conference on Functional Programming, pp. 78–91 (2005)
Walker, D.: Substructural type systems. In: Pierce, B. (ed.) Advanced Topics in Types and Programming Languages, pp. 3–43. MIT Press, Cambridge (2005)
Pfenning, F., Schürmann, C.: Twelf – a meta-logic framework for deductive systems. In: Proc. Conference on Automated Deduction, pp. 202–206 (1999)
Schürmann, C., Pfenning, F.: A coverage checking algorithm for LF. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 120–135. Springer, Heidelberg (2003)
Chen, C., Xi, H.: Combining programming with theorem proving. In: Proc. International Conference on Functional Programming, pp. 66–77 (2005)
Sheard, T., Pasalic, E.: Meta-programming with built-in type equality (extended abstract). In: International Workshop on Logical Frameworks and Meta-Languages (2004)
Mandelbaum, Y., Walker, D., Harper, R.: An effective theory of type refinements. In: Proc. International Conference on Functional Programming, pp. 213–225 (2003)
Tofte, M., Birkedal, L., Elsman, M., Hallenberg, N., Olesen, T.H., Sestoft, P.: Programming with regions in the ML Kit (for version 4). Technical report, IT University of Copenhagen (2002)
Aiken, A., Fähndrich, M., Levien, R.: Better static memory management: Improving region-based analysis of higher-order languages. In: Proc. Programming Language Design and Implementation, pp. 174–185 (1995)
Henglein, F., Makholm, H., Niss, H.: A direct approach to control-flow sensitive region-based memory management. In: Proc. Principles and Practice of Declarative Programming, pp. 175–186 (2001)
Walker, D., Crary, K., Morrisett, G.: Typed memory management in a calculus of capabilities. ACM Transactions on Programming Languages and Systems 24(4), 701–771 (2000)
Walker, D., Watkins, K.: On regions and linear types. In: Proc. International Conference on Functional Programming, pp. 181–192 (2001)
Wang, D., Appel, A.: Type-preserving garbage collectors. In: Proc. Principles of Programming Languages, pp. 166–178 (2001)
Monnier, S., Saha, B., Shao, Z.: Principled scavenging. In: Proc. Programming Language Design and Implementation, pp. 81–91 (2001)
Hawblitzel, C., Wei, E., Huang, H., Krupski, E., Wittie, L.: Low-level linear memory management. In: Proc. SPACE Workshop (2004)
DeLine, R., Fähndrich, M.: Enforcing high-level protocols in low-level software. In: Proc. Programming Language Design and Implementation, pp. 59–69 (2001)
Fähndrich, M., DeLine, R.: Adoption and focus: Practical linear types for imperative programming. In: Proc. Programming Language Design and Implementation, pp. 13–24 (2002)
Morrisett, G., Ahmed, A., Fluet, M.: L3: A linear language with locations. In: Proc. Typed Lambda Calculi and Applications, pp. 293–307 (2005)
Ahmed, A., Fluet, M., Morrisett, G.: L3: A linear language with locations. Technical Report TR-24-04, Harvard University (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fluet, M., Morrisett, G., Ahmed, A. (2006). Linear Regions Are All You Need. In: Sestoft, P. (eds) Programming Languages and Systems. ESOP 2006. Lecture Notes in Computer Science, vol 3924. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11693024_2
Download citation
DOI: https://doi.org/10.1007/11693024_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33095-0
Online ISBN: 978-3-540-33096-7
eBook Packages: Computer ScienceComputer Science (R0)