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
