Gradual typing for annotated type systems

Abstract

Refinement type systems have been proposed by a number of researchers to sharpen the guarantees of existing type systems. Examples are systems that distinguish empty and non-empty lists by type, taint tracking and information flow control, dimension analysis, and many others. In each case, the type language is extended with annotations that either abstract semantic properties of values beyond the capabilities of the underlying type language (e.g., empty and non-empty lists) or they express extrinsic properties that are not locally checkable (e.g., taintedness, dimensions).