Higher-order unification, polymorphism, and subsorts

Tobias Nipkow
This paper analyses the problems that arise in extending Huet’s higher-order unification algorithm from the simply typed λ-calculus to one with type variables. A simple, incomplete, but in practice very useful extension to Huet’s algorithm is discussed. This extension takes an abstract view of types. As a particular instance we explore a type system with ML-style polymorphism enriched with a notion of sorts. Sorts are partially ordered and classify types, thus giving rise to an...
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.