[isabelle-dev] Interest in isomorphic transfer?
schropp at in.tum.de
Mon Aug 22 21:07:29 CEST 2011
On 08/20/2011 07:34 PM, Andreas Schropp wrote:
> On 08/20/2011 01:18 AM, Florian Haftmann wrote:
>>> In the long run, I would prefer to see flexible transport
>>> machinery to move stuff between isomorphic types.
>> What is a different – and in itself valuable – thing is the matter of
>> »transport« mentioned by Alex, something which also I am eager to see
>> one day.
> I'll just be blunt: would someone in Munich be interested
> to supervise a diploma thesis on the matter?
In case isabelle-dev is wondering: the locals are interested
and my optimism about this could not be higher, now that
I have written up the rule system I had in mind and still
don't see any problems.
More information about the isabelle-dev