We present an abstract model of computer memory, in the form of directed, labelled graphs with simple transitions corresponding to valid memory operations. We also introduce a refinement of this basic model of memory that incorporates features of memory management. After giving some examples of how this refined model captures various garbage collection algorithms, we discuss a proof under development that the two representations are behaviorally equivalent.
This will be an informal presentation of proofs that are being carried out in the theorem prover Coq.