[isabelle-dev] auto raises a TYPE exception
lp15 at cam.ac.uk
Thu May 30 15:11:36 CEST 2013
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.
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).
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev