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