Type-preserving garbage collectors
- 1 January 2001
- proceedings article
- Published by Association for Computing Machinery (ACM)
- Vol. 36 (3) , 166-178
- https://doi.org/10.1145/360204.360218
Abstract
By combining existing type systems with standard type-based compilation techniques, we describe how to write strongly typed programs that include a function that acts as a t racing garbage collector for the program. Since the garbage collector is an explicit function, we do not need to provide a t rusted garbage collector as a runtime service to manage memory.Since our language is strongly typed, the standard type soundness guarantee "Well typed programs do not go wrong" is extended to include the collector. Our type safety guarantee is non-trivial since not only does it guarantee the type safety of the garbage collector, but it guarantees that the collector preservers the type safety of the program being garbage collected. We describe the technique in detail and report performance measurements for a few microbench-marks as well as sketch the proofs of type soundness for our system.Keywords
This publication has 23 references indexed in Scilit:
- Alias TypesPublished by Springer Nature ,2000
- Efficient and safe-for-space closure conversionACM Transactions on Programming Languages and Systems, 2000
- From ML to Ada: Strongly-typed language interoperability via source translationJournal of Functional Programming, 1998
- Typed closure conversionPublished by Association for Computing Machinery (ACM) ,1996
- Empirical and analytic study of stack versus heap cost for languages with closuresJournal of Functional Programming, 1996
- Java intermediate bytecodesACM SIGPLAN Notices, 1995
- The Boyer benchmark meets linear logicACM SIGPLAN Lisp Pointers, 1993
- Lively linear LispACM SIGPLAN Notices, 1992
- The treadmillACM SIGPLAN Notices, 1992
- An efficient machine-independent procedure for garbage collection in various list structuresCommunications of the ACM, 1967