[Club2] talk by Ondrej Kunkar: tomorrow, Tuesday July 9, 16:30, Turing

[Andrei Popescu]

Dear All, 

Tomorrow, Ondra will inaugurate the ITP 2013 rehearsal series.  

Andrei 

Data Refinement in Isabelle/HOL
Ondrej Kuncar
joint work with Florian Haftmann, Alexander Krauss and Tobias Nipkow
====================================================================
Tue. July 9, 16:30, Alan Turing

The talk shows how the code generator of Isabelle/HOL supports data 
refinement, i.e., providing efficient code for operations on abstract 
types, e.g., sets or numbers. This allows all tools that employ code 
generation, e.g., Quickcheck or proof by evaluation, to compute with 
these abstract types. At the core is an extension of the code generator 
to deal with data type invariants. In order to automate the process of 
setting up specific data refinements, two packages for transferring 
definitions and theorems between types are exploited.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20130708/0289b038/attachment.html>