Some Uses of the Intersection Type

by Stuart F. Allen, Robert L. Constable
1998-1999

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?).

Some Uses of the Intersection Type

by Stuart F. Allen, Robert L. Constable 1998-1999

by Stuart F. Allen, Robert L. Constable
1998-1999