skip to main content
10.1145/604131.604147acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
Article

A type theory for memory allocation and data layout

Published:15 January 2003Publication History

ABSTRACT

Ordered type theory is an extension of linear type theory in which variables in the context may be neither dropped nor re-ordered. This restriction gives rise to a natural notion of adjacency. We show that a language based on ordered types can use this property to give an exact account of the layout of data in memory. The fuse constructor from ordered logic describes adjacency of values in memory, and the mobility modal describes pointers into the heap. We choose a particular allocation model based on a common implementation scheme for copying garbage collection and show how this permits us to separate out the allocation and initialization of memory locations in such a way as to account for optimizations such as the coalescing of multiple calls to the allocator.

References

  1. Jawahar Chirimar, Carl A. Gunter, and Jon G. Riecke. Reference counting as a computational interpretation of linear logic. Journal of Functional Programming, 6(2):195--244, 1996.]]Google ScholarGoogle ScholarCross RefCross Ref
  2. Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Mark Plesko, and Kenneth Cline. A certifying compiler for Java. In Proceedings of the Conference on Programming Language Design and Implementation (PLDI'00), pages 95--107, Vancouver, Canada, June 2000. ACM Press.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. Karl Crary and Greg Morrisett. Type structure for low-level programming langauges. In Twenty-Sixth International Colloquium on Automata, Languages, and Programming, volume 1644 of Lecture Notes in Computer Science, pages 40--54, Prague, Czech Republic, July 1999. Springer-Verlag.]] Google ScholarGoogle Scholar
  4. Karl Crary and Stephanie Weirich. Flexible type analysis. In 1999 ACM International Conference on Functional Programming, Paris, France, September 1999. ACM Press.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. A. Igarashi and N. Kobayashi. Garbage collection based on a linear type system, 2000.]]Google ScholarGoogle Scholar
  6. T. Jim, G. Morrisett, D. Grossman, M. Hicks, J. Cheney, and Y. Wang. Cyclone: A safe dialect of c, June 2002.]]Google ScholarGoogle Scholar
  7. Naoki Kobayashi. Quasi-linear types. In Conference Record of POPL 99: The 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, Texas, pages 29--42, New York, NY, 1999.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. Y. Minamide. A functional represention of data structures with a hole. In Conference Record of the 25th Symposium on Principles of Programming Languages (POPL '98), 1998.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  9. Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. In Second Workshop on Compiler Support for System Software, pages 25--35, Atlanta, Georgia, May 1999.]]Google ScholarGoogle Scholar
  10. Greg Morrisett and Robert Harper. Semantics of memory management for polymorphic languages. In A. Gordon and A. Pitts, editors, Higer Order Operational Techniques in Semantics. Newton Institute, Cambridge University Press, 1997.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):527--568, 1999.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. George C. Necula and Peter Lee. The design and implementation of a certifying compiler. In Keith D. Cooper, editor, Proceedings of the Conference on Programming Language Design and Implementation (PLDI'98), pages 333--344, Montreal, Canada, June 1998. ACM Press.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. Leaf Petersen, Robert Harper, Karl Crary, and Frank Pfenning. A type theory for memory allocation and data layout. Technical Report CMU-CS-02-171, Department of Computer Science, Carnegie Mellon University, December 2002.]]Google ScholarGoogle Scholar
  14. Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11(4):511--540, 2001.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  15. Jeff Polakow. Ordered linear logic and applications. PhD thesis, Carnegie Mellon University, June 2001. Available as Technical Report CMU-CS-01-152.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. Jeff Polakow and Frank Pfenning. Natural deduction for intuitionistic non-commutative linear logic. In J.-Y. Girard, editor, Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications (TLCA'99), pages 295--309, L'Aquila, Italy, April 1999. Springer-Verlag LNCS 1581.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. Jeff Polakow and Frank Pfenning. Relating natural deduction and sequent calculus for intuitionistic non-commutative linear logic. In Andre Scedrov and Achim Jung, editors, Proceedings of the 15th Conference on Mathematical Foundations of Programming Semantics, New Orleans, Louisiana, April 1999. Electronic Notes in Theoretical Computer Science, Volume 20.]]Google ScholarGoogle Scholar
  18. Jeff Polakow and Frank Pfenning. Properties of terms in continuation-passing style in an ordered logical framework. In J.Despeyroux, editor, Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications (TLCA'99), Santa Barbara, California, June 2000.]]Google ScholarGoogle Scholar
  19. Zhong Shao. An overview of the FLINT/ML compiler. In 1997 Workshop on Types in Compilation, Amsterdam, June 1997. ACM SIGPLAN. Published as Boston College Computer Science Department Technical Report BCCS-97-03.]]Google ScholarGoogle Scholar
  20. Frederick Smith, David Walker, and Greg Morrisett. Alias types. Lecture Notes in Computer Science, 1782, 2000.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  21. David Tarditi, Greg Morrisett, Perry Cheng, Chris Stone, Robert Harper, and Peter Lee. TIL: A type-directed optimizing compiler for ML. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 181--192, Philadelphia, PA, May 1996.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  22. David N. Turner and Philip Wadler. Operational interpretations of linear logic. Theoretical Computer Science, 227(1--2):231--248, 1999.]] Google ScholarGoogle ScholarDigital LibraryDigital Library
  23. Hongwei Xi and Frank Pfenning. Eliminating array bound checking through dependent types. In Keith D. Cooper, editor, Proceedings of the Conference on Programming Language Design and Implementation (PLDI'98), pages 249--257, Montreal, Canada, June 1998. ACM Press.]] Google ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. A type theory for memory allocation and data layout

          Recommendations

          Comments

          Login options

          Check if you have access through your login credentials or your institution to get full access on this article.

          Sign in
          • Published in

            cover image ACM Conferences
            POPL '03: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages
            January 2003
            308 pages
            ISBN:1581136285
            DOI:10.1145/604131
            • cover image ACM SIGPLAN Notices
              ACM SIGPLAN Notices  Volume 38, Issue 1
              January 2003
              298 pages
              ISSN:0362-1340
              EISSN:1558-1160
              DOI:10.1145/640128
              Issue’s Table of Contents

            Copyright © 2003 ACM

            Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

            Publisher

            Association for Computing Machinery

            New York, NY, United States

            Publication History

            • Published: 15 January 2003

            Permissions

            Request permissions about this article.

            Request Permissions

            Check for updates

            Qualifiers

            • Article

            Acceptance Rates

            POPL '03 Paper Acceptance Rate24of126submissions,19%Overall Acceptance Rate824of4,130submissions,20%

            Upcoming Conference

            POPL '25

          PDF Format

          View or Download as a PDF file.

          PDF

          eReader

          View online with eReader.

          eReader