A subtyping 0 is entailed by a set of subtyping constraints C, written C j= 0, if every valuation (mapping of type variables to ground types) that satisfies C also satisfies 0. ...
Abstract. We study entailment of structural and nonstructural recursive subtyping constraints. Constraints are formal inequalities between type expressions, interpreted over an ord...
Entailment of subtype constraints was introduced for constraint simplification in subtype inference systems. Designing an efficient algorithm for subtype entailment turned out to...
Decidability of non-structural subtype entailment is a long standing open problem in programming language theory. In this paper, we apply automata theoretic methods to characterize...