Abstract

We will present a perspicuous example using the intersection type to express specifications from which one may extract recursive programs (a while-loop in this case), that do not use their bounds.

We will also discuss the use of "guarded types", which are intersection types Isect(x:A.B) in which B does not depend on x. This type constructor is a variation on Malcolm and Chisolm's so-called "polymorphic function" type constructor, (1989?).