[Club2] talk by Florian Haftmann, Wed. April 3, Tarski

[Andrei Popescu]

Dear All,  
Next week, Florian will visit us and talk about his recent work on Isabelle's big operators.  
Best regards,   Andrei 
Florian HaftmannWork on big operators======================================================Wed. April. 3, 14:00, Room 01.09.011 ("Alfred Tarski") 
»Big Operators« are a certain class of operators which lift a binaryoperator to (finite) (multi-)sets. We explain the rationale behindrecent renovation in Isabelle/HOL which aims to make definition andapplication of Big Operators more handsome and less cryptic. A key roleis taken by the Isabelle module system, particularly sublocaleinterpretation with mixin equations.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20130325/22ebae66/attachment.html>