Modern approaches to garbage collection (GC) require
information about which variables and fields contain GC-managed
pointers. Interprocedural flow analysis can be used to eliminate
otherwise unnecessary heap allocated objects (unboxing), but
must maintain the necessary GC information. We define a core language
which models compiler correctness with respect to the GC, and develop
a correctness specification for interprocedural unboxing
optimizations. We prove that any optimization which satisfies our
specification will preserve GC safety properties and program
semantics, and give a practical unboxing algorithm satisfying this
specification.