[Club2] Fw: Talks by Alex Krauss and Makarius Wenzel: Wed. Dec 19, 14:00, Church -- abstract as plain text attachment

[Andrei Popescu]

Reminder: Talk by Alex Krauss today at 13:30 and by Makarius Wenzel at 14:00.
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.

Makarius
 WenzelIsabelle/jEdit jam session====================================================Wed. Dec. 19, 14:00, Room 01.09.014 ("Alonzo Church") 
After almost 5 years of development, Isabelle/jEdit is moving towardsits 3rd official release early 2013.  Many things have been achieved,many things are still missing.  The whole complex of explaining theconcepts
 behind the Prover IDE is still underdeveloped, but see therecent paper
 http://www4.in.tum.de/~wenzelm/papers/async-repl.pdf andits references.
Instead of giving another scientific talk, the purpose of this relaxedsession just before Christmas is to see what works out in practice andwhat not -- to exchange ideas and techniques for using the systemeffectively in everyday life of theorem proving and librarymaintenance.  Users of Isabelle/jEdit are welcome to contribute
 theirown tips and tricks.  Non-users (or rather not-yet-users) may learnthat there is life beyond Emacs, and actually some conceptual progressin prover interaction after several decades.


-----Inline Attachment Follows-----

_______________________________________________
Club2 mailing list
List page: https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/club2
Webpage with calendar: http://www21.in.tum.de/club2
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20121219/10b172dc/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: abstract.txt
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20121219/10b172dc/attachment.txt>