[Club2] Wed. Jul 20 (Today!), 14:00: Alexander Krauss

[Alexander Krauss]

Dear all,

This week I have the pleasure to fill our Club2 slot myself, with a talk 
on recent experiments with code generations and the quotient package.



Simpler Data Refinement with Quotients
====================================================
Wed. Jul 20, 14:00, MI 00.09.055 ("Alan Turing")

We give an overview over problems related to the automatic
transport of theorems from one type to another. Starting from the
original motivation, data refinement during code generation, we
explore the possibilities and the existing implementations of
related mechanisms in Isabelle. In particular, we show how
formalizations over ordinary sets can be automatically transported
over to the isomorphic but executable copy "'a Set" (commonly
known as Cset.set). This approach could be a cornerstone in a
general and practical approach to data refinement.

Moreover, we give some comparison of the existing tools
"transfer" (by Chaieb and Avigad) and the quotient package (by
Kaliszyk and Urban), exploring the question whether these tools
could be unified. This document does not present finished solutions
in this regard. Rather, its purpose is to give a better
understanding of the problems and bring relevant information
together that has been disconnected, hard to find, or undocumented.

http://www4.in.tum.de/~krauss/papers/refinement.pdf