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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
