We present a programming language, model, and logic appropriate for
implementing and reasoning about a memory management system. We then
state what is meant by correctness of a copying garbage collector, and
employ a variant of the novel separation logicsto formally specify partial correctness of Cheney's copying garbage collector. Finally, we prove that our implementation of Cheney's algorithm meets its specification, using thelogic we have given, and auxiliary variables.
