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

[Andrei Popescu]

________________________________
 From: Andrei Popescu <uuomul at yahoo.com>
To: club2 <club2 at mailbroy.informatik.tu-muenchen.de> 
Sent: Thursday, July 11, 2013 3:26 PM
Subject: [Club2] talk Peter Lammich, Tue. July 16, 11:00, Turing
 


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.
_______________________________________________
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/20130715/f81eabf8/attachment.html>