BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Deep Embedding of a Decidable Fragment of Separation Logic in HO
 L - Thomas Tuerk (University of Cambridge)
DTSTART:20070626T120000Z
DTEND:20070626T130000Z
UID:TALK7416@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Smallfoot is a tool to automatically check separation logic sp
 ecifications of imperative programs. It uses a decidable fragment of separ
 ation logic. In this talk\, I will present a deep embedding of this fragme
 nt of separation logic in HOL.\nAdditionally\, I will present a HOL implem
 entation of a decision procedure for entailments\, which is based on the i
 nferences used by Smallfoot.
LOCATION:Computer Laboratory\, William Gates Building\, Room GS15
END:VEVENT
END:VCALENDAR