On the use of subtypes in ABEL

ABEL is a wide spectrum language developed at the University of Oslo. The applicative core of ABEL is a typed first order language with subtypes and partial functions. The paper presents a constructive fragment of the core, based on terminating generator induction. We show how subtypes can be used to augment expressiveness and strengthen syntactic controls