Subject: An abstract formulation of memory management
Jour: 26/09/97 (Vendredi 26 septembre)

           http://pauillac.inria.fr/bin/calendar/Seminaires


                             S E M I N A I R E
       ____               ____                             ___                
      /    _   _         /     __     __  /_  _   /       /   |  _   __   _   
     /    / \ / \  ___  /     /  | / /_  /   __| /  ___  /___/  __| /  | __|  
    |___  |_/ |_/      |____ /    / __/ |_  |_/ |_      /      |_/ /    |_/   
               /                                                              
              /                                                               
                          I N R I A - Rocquencourt, 
                    Salle de confe'rence du batiment 11

                        Vendredi 26 septembre, 10h30


                            -------------------
                             Healfdene Goguen
                            -------------------

               LFCS, Dept. of Computer Science, Univ. of Edinburg
                                      

        ============================================================
             An abstract formulation of memory management
        ============================================================

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.
The talk  is an overview of  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.