Positive recursive type assignment

Abstract

We consider several different definitions of type assignment with positive recursive types, from the point of view of their typing ability. We discuss the relationships between these systems. In particular, we show that the class of typable pure lambda terms remains the same for different type disciplines involving positive type fixpoints, and that type reconstruction is decidable.