[Club2] Diploma thesis presentation by Andreas Schropp -- Fri. May 11, 2 PM, Turing

[Andrei Popescu]

Dear All,  
The coming Friday, Andreas will present his diploma thesis work.      
Best regards,   Andrei 

Andreas SchroppInstantiating deeply embedded many-sorted theoriesinto HOL types in Isabelle  ====================================================Fri. May 11, 14:00, MI 00.09.055 ("Alan Turing")  
The development of tools for theorem proving still needs in-depthknowledge of the programming interface of the theorem prover.A large class of packages can be understood as HOL theoriesparameterized on many-sorted signatures, so we try to improve thesituation by providing a paradigm for formulating such meta-theoriesand infrastructure for animating them.We applied the paradigm and infrastructure in the construction of apackage for non-freely generated datatypes.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20120505/c1699030/attachment.html>