| A Partial Type Checking Algorithm for Type: Type (2009) | |||||||||||||||||
Abstract | |||||||||||||||||
| 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. Keywords: | |||||||||||||||||
Publication details | |||||||||||||||||
| |||||||||||||||||