## Paper: Subtype inequalities (at LICS 1992)

**Jerzy Tiuryn**

### Abstract

The satisfiability problem for subtype inequalities in simple types is studied. The naive algorithm that solves this problem runs in nondeterministic exponential time for every predefined poset of atomic subtypings the satisfiability problem for subtype inequalities is PSPACE-hard. On the other hand, it is proved that if the poset of atomic subtypings is a disjoint union of lattices, then the satisfiability problem for subtype inequalities is solvable in PTIME. This result covers the important special case of the unification problem that can be obtained when the atomic subtype relation is equality

### BibTeX

@InProceedings{Tiuryn-Subtypeinequalities, author = {Jerzy Tiuryn}, title = {Subtype inequalities}, booktitle = {Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (LICS 1992)}, year = {1992}, month = {June}, pages = {308--315}, location = {Santa Cruz, CA, USA}, publisher = {IEEE Computer Society Press} }