Lambda the Ultimate

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?