An abstract formulation of memory management

This talk will discuss ongoing work in progress on memory management by the LEGO project, including John Longley, Rod Burstall, Paul Jackson and me, together with Richard Brooksby and David Jones at Harlequin Ltd.

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.

Healfdene Goguen
Last modified: Mon Jul 14 17:46:42 BST 1997