BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Computer Laboratory Automated Reasoning Group Lunc
 hes
SUMMARY:Rough-and-ready proof reconstruction - Nik Sultana
DTSTART;TZID=Europe/London:20110301T131500
DTEND;TZID=Europe/London:20110301T141500
UID:TALK29333AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/29333
DESCRIPTION:This talk addresses the following question: "if we
  have a proof in one system\, how do we check it u
 sing a different system?" . The motivations for as
 king this question are twofold: one might wish to 
 move proofs of propositions between different syst
 ems\; one might also wish to use a 'safer' system 
 to check a proof\, in the spirit of de Bruijn. Dur
 ing the talk I will describe an approach to proof 
 reconstruction which relies on the existing intern
 al automation of Isabelle/HOL to check proofs prod
 uced by Leo-II. This is made possible by Isabelle/
 HOL's good level of automation. I will discuss som
 e experimental results which suggest a measure of 
 the strength of Isabelle/HOL's internal automation
  relative to Leo-II.
LOCATION:Computer Laboratory\, William Gates Building\, Roo
 m SS03
CONTACT:William Denman
END:VEVENT
END:VCALENDAR