In MemBalancer, my student Marisa and I came up with a novel correctness property for garbage collection heap limits, which we called "compositionality", derived compositional heap limits for a basic one-generation garbage collector, and showed that this new heap limit lead to big reductions in memory usage for Chrome's V8 JavaScript runtime. But actually V8 uses a generational GC, and compositional heap limits for that are much harder to derive. Compositional heap limits Any time you have a ...