BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Interfacing two similar HOLs - Nik Sultana (University of Cambridg
 e)
DTSTART:20100309T130000Z
DTEND:20100309T140000Z
UID:TALK22761@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:In this talk I will describe ongoing work to interface the the
 orem-provers Isabelle/HOL and LEO-II. Both systems accept encodings in sim
 ilar dialects of classical higher-order logic but offer contrasting levels
  of support in terms of ease-of-encoding and automation: Isabelle/HOL offe
 rs a comfortable setup of definitional extensions\, but offers moderate au
 tomation\; whereas LEO-II is definitionally spartan but promises a high de
 gree of automation. The integration of these two tools is desirable since 
 it would yield a composite which enjoys the good qualities of both tools.\
 n
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR