[isabelle-dev] auto raises a TYPE exception

[Tobias Nipkow]

Am 30/05/2013 13:49, schrieb Tobias Nipkow:
> Am 30/05/2013 13:41, schrieb Lawrence Paulson:
>> The only question is whether Isabelle is important enough for such work to be seen as significant in a wider context.
> 
> Makarius is right, the interaction of schematic type variables and HOU has never
> been nailed down properly and would be of interest to a larger community.

Correction: my CTRS 90 paper contains a pen-and-paper formalisation of the full
HOU algorithm expressed as transformation rules, but without proofs. It is the
pattern unification algorithm where the polymorphic case seems not to have been
examined in any detail (except probably in my head at the time).

Tobias

> Tobias
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>