[isabelle-dev] auto raises a TYPE exception

Tobias Nipkow nipkow at in.tum.de
Thu May 30 14:04:49 CEST 2013

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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list