BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Cyclic Proofs of Program Termination in Separation Logic - James B
 rotherston\, Imperial College
DTSTART:20070615T130000Z
DTEND:20070615T140000Z
UID:TALK7605@talks.cam.ac.uk
CONTACT:Matthew Parkinson
DESCRIPTION:We present a new approach to proving termination of simple imp
 erative programs\, encapsulated in a Hoare-style proof system whose judgem
 ents express termination from a given program index and under a given sepa
 ration logic precondition.  Moreover\, proofs in our system are *cyclic pr
 oofs* (i.e. tree proofs containing some loops) which satisfy a global trac
 e condition - corresponding to an infinite descent principle for the induc
 tively defined predicates in the preconditions - that ensures soundness.  
 We demonstrate the viability of our system via simple examples\, and specu
 late on its potential applications.\n\nThis is joint work with Cristiano C
 alcagno\, also at Imperial\, and Richard Bornat\, at Middlesex University\
 , London.
LOCATION:FW11
END:VEVENT
END:VCALENDAR