BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Integration of SMT Solvers with ITPs - There and Back Again - Tjar
 k Weber (University of Cambridge)
DTSTART:20100302T130000Z
DTEND:20100302T140000Z
UID:TALK22760@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:How can interactive theorem provers benefit from SMT solvers? 
 Can we integrate SMT solvers without enlarging the trusted code base? In t
 his talk I will present an integration of SMT solvers with the HOL4 and Is
 abelle/HOL theorem provers. First translations from higher-order\nlogic in
 to the input languages of SMT solvers are described. Then LCF-style proof 
 reconstruction for the SMT solver Z3 is explained\, with a focus on effici
 ency. Our implementations outperform previous ones by several orders of ma
 gnitude.  They show that LCF-style proof checking is\nfeasible even for la
 rge SMT proofs with millions of inferences.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR