BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Holfoot - A separation logic tools inside HOL 4 - Thomas Tuerk (Un
 iversity of Cambridge)
DTSTART:20100126T130000Z
DTEND:20100126T140000Z
UID:TALK22755@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:In this talk I will present the current status of my formalisa
 tion of Smallfoot inside HOL 4. Whereas my last talk focused on some techn
 ical stuff in the background\, I will present a high-level view of Holfoot
  in this one. \n\nAfter a short introduction\, the "web-interface of Holfo
 ot":http://holfoot.heap-of-problems.org will be presented. This interface 
 is limited in the sense that it does not support interaction. I will incre
 ase the level of interaction during the talk and end the demonstration wit
 h a fully functional verification of inserting a value into a red-black tr
 ee. I hope to convince the audience that Holfoot combines the power of an 
 interactive theorem prover with the automation for separation logic in a n
 atural way.\n\nAs usual the talk will stop with a discussion of current is
 sues and a plans for future work.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR