Modern approaches to garbage collection (<em>GC</em>) require
information about which variables and fields contain GC-managed
pointers.  Interprocedural flow analysis can be used to eliminate
otherwise unnecessary heap allocated objects (<em>unboxing</em>), 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.