[Club2] talk Peter Lammich, Tue. July 16, 11:00, Turing

[Andrei Popescu]

Dear All, 

Peter will rehears his ITP talk the coming Tuesday.

Cheers, 
   Andrei 

Automatic Data Refinement

Peter Lammich
====================================================================
Tue. July 16, 11:00, Alan Turing

We present the Autoref tool for Isabelle/HOL, which automatically
refines algorithms specified over
abstract concepts like maps and sets to algorithms over concrete
implementations like red-black-trees, and
produces a refinement theorem. 
It is based on ideas borrowed from relational parametricity due to
Reynolds and Wadler.

The tool allows for rapid prototyping of verified, executable
algorithms. Moreover, it can be configured to fine-tune
the result to the user's needs. Our tool is able to automatically
instantiate generic algorithms, which greatly simplifies
the implementation of executable data structures.

Thanks to its integration with the Isabelle Refinement Framework
and the Isabelle Collection Framework, Autoref can be used as a backend
to a stepwise refinement based development approach,
having access to a rich library of verified data structures. We have
evaluated the tool by synthesizing efficiently executable
refinements for some complex algorithms, as well as by implementing a
library of generic algorithms for maps and sets.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20130711/cb7480d9/attachment.html>