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.
- 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 ScholarCross Ref
- 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 ScholarDigital Library
- 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 Scholar
- Karl Crary and Stephanie Weirich. Flexible type analysis. In 1999 ACM International Conference on Functional Programming, Paris, France, September 1999. ACM Press.]] Google ScholarDigital Library
- A. Igarashi and N. Kobayashi. Garbage collection based on a linear type system, 2000.]]Google Scholar
- T. Jim, G. Morrisett, D. Grossman, M. Hicks, J. Cheney, and Y. Wang. Cyclone: A safe dialect of c, June 2002.]]Google Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11(4):511--540, 2001.]] Google ScholarDigital Library
- Jeff Polakow. Ordered linear logic and applications. PhD thesis, Carnegie Mellon University, June 2001. Available as Technical Report CMU-CS-01-152.]] Google ScholarDigital Library
- 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 ScholarDigital Library
- 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 Scholar
- 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 Scholar
- 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 Scholar
- Frederick Smith, David Walker, and Greg Morrisett. Alias types. Lecture Notes in Computer Science, 1782, 2000.]] Google ScholarDigital Library
- 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 ScholarDigital Library
- David N. Turner and Philip Wadler. Operational interpretations of linear logic. Theoretical Computer Science, 227(1--2):231--248, 1999.]] Google ScholarDigital Library
- 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 ScholarDigital Library
Index Terms
A type theory for memory allocation and data layout
Recommendations
A type theory for memory allocation and data layout
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 ...
Formalizing Type Operations Using the “Image” Type Constructor
In this paper we introduce a new approach to formalizing certain type operations in type theory. Traditionally, many type constructors in type theory are independently axiomatized and the correctness of these axioms is argued semantically. In this paper ...
A functional programmer's guide to homotopy type theory
ICFP '16Dependent type theories are functional programming languages with types rich enough to do computer-checked mathematics and software verification. Homotopy type theory is a recent area of work that connects dependent type theory to the mathematical ...
Comments