BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:New tools in HOL 4 - Consequence Conversions\, Quantifier Heuristi
 cs\, Styles - Thomas Tuerk (University of Cambridge)
DTSTART:20091124T130000Z
DTEND:20091124T140000Z
UID:TALK19691@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Nik Sultana canceled his talk\, so I'm stepping in. Nik's talk
  will probably be given next term.\n\nIn this talk\, I will present some t
 ools developed for my implementation of separation logic in HOL 4. In part
 icular\, I will present \n\n* Consequence Conversions\n* Quantifier Heuris
 tics\n* pretty-printing with styles\n\nFinally\, I will give a very short 
 demo on how these tools are used in my formalization of separation logic. 
 This talk will contain some details on HOL 4\, but may be interesting to n
 on HOL 4 users as well.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR