Semantics of Memory Management for Polymorphic Languages

In Semantics of Memory Management for Polymorphic Languages (1997) Greg Morrisett and Robert Harper

...present a static and dynamic semantics for an abstract machine that evaluates expressions of a polymorphic programming language. Unlike traditional semantics, our abstract machine exposes many important issues of memory management, such as value sharing and control representation. We prove the soundness of the static semantics with respect to the dynamic semantics using traditional techniques. We then show how these same techniques may be used to establish the soundness of various memory management strategies, including type-based, tag-free garbage collection; tail-call elimination; and environment strengthening.

This should keep the formal semantics LtUers happy for a little while. But is all the machinery necessary? Is there an easier way to prove that garbage can be thrown out?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Garbage Collection Research

If you're interested in simpler models of garbage collection or space usage more generally, you should look at Morrisett, Felleisen and Harper - Abstract Models of Memory Management (cited by the above paper), and also Clinger 1998, Proper tail recursion and space efficiency.

Good references. I hadn't

Good references. I hadn't come across them before.