A Partial Type Checking Algorithm for Type:Type

We analyze a partial type checking algorithm for the inconsistent domain-free pure type system Type:Type (λ⁎). We show that the algorithm is sound and partially complete using a coinductive specification of algorithmic equality. This entails that the algorithm will only diverge due to the presence of diverging computations, in particular it will terminate for all typeable terms.