[Club2] Talk by Alex Kraus: Wed. Dec. 19, Church

[Andrei Popescu]

Dear All,
On the "Makarius day", we have an additional talk by Alex Kraus on proof exchange between HOL Light and Isabelle/HOL.   This is at 13:30, half an hour before Makarius's talk. Details follow.
Regards,    Andrei 
Alex KraussTowards scalable LCF-style proof exchange(joint work with Cezary Kaliszyk)====================================================Wed. Dec. 19, 13:30, Room 01.09.014 ("Alonzo Church") 
All existing translations between proof assistants have been notoriously sluggy,resource-demanding, and do not scale to large developments, which has lead tothe general perception that the whole approach is probably not
 practical. We aimto show that the observed inefficiencies are not inherent, but merely adeficiency of the existing implementations. We do so by providing a newimplementation of a theory import from HOL Light to Isabelle/HOL, which achievesdecent performance and scalability mostly by avoiding the mistakes of the past.
After some preprocessing, our tool can import large HOL Light developmentsfaster than HOL Light processes them. Our main
 target and motivation is theFlyspeck development, which can be imported in a few hours on commodity hardware.
This talk outlines some design considerations and presents a few of ourextensive measurements, which reveal interesting insights in the low-levelstructure of larger proof developments.



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20121203/747d535d/attachment.html>