[isabelle-dev] auto raises a TYPE exception

[Lawrence Paulson]

I know that there have been a lot of other papers on higher-order unification expressed as an inference system. Maybe Dale Miller knows more about this work.
Larry

On 30 May 2013, at 13:04, Tobias Nipkow <nipkow at in.tum.de> wrote:

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