Earlier work on subtyping has focused on the problem of constructing a typing for a given program. This paper considers a slightly different problem: Given a lambda term, is the corresponding constraint system consistent? An O(n3) algorithm for checking the consistency of constraint systems is presented, where n is the size of the constraint system.
The paper also considers the problem of derivability, i.e., whether a property can be derived from the corresponding constraint system and gives an O(n3) algorithm for checking derivability of a class of constraints.
Available as PDF (280 kB, no cover)
Download BibTeX entry.