BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Reasoning about Code Pointers (Separation Logic for Higher-Order S
 tore) - Bernhard Reus\, University of Sussex
DTSTART:20061103T140000Z
DTEND:20061103T150000Z
UID:TALK5665@talks.cam.ac.uk
CONTACT:Tom Ridge
DESCRIPTION:Separation Logic is a sub-structural logic that supports local
  reasoning for imperative programs with heaps. It is designed to elegantly
   describe  sharing and aliasing properties of  heap structures\, thus  fa
 cilitating the verification of programs with pointers. So far\, various fl
 avours of separation logic have been developed for heaps containing record
 s  of basic data types. Yet\, languages like C or ML also allow  procedure
 s to be stored on the heap.  Such type of heap is commonly referred to as 
  "higher-order store''.\n> This talk addresses the problem of lifting Sepa
 ration Logic from first-order to higher-order store. To that end we endow 
 a simple language including dynamic memory management with a Hoare-style l
 ogic featuring Separation Logic connectives.  To prove soundness\, Denotat
 ional Semantics is employed throughout but not just for conceptual clarity
 . Modeling higher-order store as recursive domain enables us to use powerf
 ul (and well established) results from Domain Theory.   This approach also
  admits an elegant re-use of a proof rule  we introduced in previous work 
 to deal with recursion through the store.\n\nThis is joint work with Jan S
 chwinghammer\, Programming Systems Lab\, Saarland University.\n
LOCATION:FW11
END:VEVENT
END:VCALENDAR