[isabelle-dev] Interest in isomorphic transfer?

[Andreas Schropp]

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?
The cognoscenti know that I have found a solution (at least on
paper) via reflection in ZF a while ago, but I guess the interest
in ZF is limited right now.
I am optimistic that my reflection-based theorem in ZF
can be recast in HOL as a HOAS-directed constructive meta function
(think: Twelf-style function definition).
For some reason I am in possession of a well-behaved animation principle
for HOAS-directed meta-recursions, so don't mistake me for a
science-fiction author just now.

If someone is interested, I will provide you with a write-up of
these thoughts next semester.


Cheers,
   Andy