[isabelle-dev] auto raises a TYPE exception

[Makarius]

On Tue, 28 May 2013, Tobias Nipkow wrote:

> Am 28/05/2013 13:34, schrieb Lawrence Paulson:
>> Historical note: when the original high-order unification code was written, there was no user-level polymorphism. If my memory is correct, the TVar constructor did not even exist. Polymorphism was only used for type inference in terms.
>
> correct. i added that part of the code in about 1990. of course i never 
> proved anything about it.

The complexity of the implementation is one thing, but how about the 
algorithmic ideas?

Is "Huet + schematic polymorphism" and "Miller + schematic polymorphism" 
sufficiently well-understood to make a nice formalization from that? 
Lets say with the de-Bruijn toolbox that Stefan had in his entry to 
POPLmark (which has the advantage that it is close to what is actually 
done in Isabelle/ML, unlike Nominal datatypes).


 	Makarius