Correctness of a Garbage Collector via Local Reasoning

We give a programming language, model, and logic appropriate for implementing and reasoning about a memory management system. We then outline what is meant by correctness of a copying garbage collector, and employ a variant of the novel Separation Logics to formally specify correctness. We then prove that our implementation meets its specification, using the logic we have given, and auxiliary variables.