Subtyping, consistency and derivability

Sven-Olof Nyström

May 2014

Abstract:

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(n³) 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(n³) algorithm for checking derivability of a class of constraints.

Available as PDF (280 kB, no cover)

Download BibTeX entry.