A garbage collection (GC) scheme --- what we call type inference GC --- that dynamically performs type inference is studied. In contrast to conventional garbage collection that can collect only unreachable objects, this scheme can collect objects that are reachable yet semantically garbage. The idea is to utilize ML-like type information that can tell whether or not each object may be used in the rest of computation. There has been some work studying algorithms of the GC scheme. However, their descriptions are either too informal or too abstract, and as a result, either correctness of their algorithms is not so clear, or there remains a gap between models and implementation. Moreover, no formal framework has dealt with polymorphism. This paper presents a formal framework that can directly serve both as specifications for implementing the GC scheme and as a foundation for discussing it. Specifically, on top of a language that reflects a usual execution scheme for functional languages, w...