  Refinement types turn typechecking into lightweight verification. The classic
form of refinement type is the datasort refinement, in which datasorts identify
subclasses of inductive datatypes.
  Existing type systems for datasort refinements require that all the
refinements of a type be specified when the type is declared; multiple
refinements of the same type can be obtained only by duplicating type
definitions, and consequently, duplicating code.
  We enrich the traditional notion of a signature, which describes the
inhabitants of datasorts, to allow re-refinement via signature extension,
without duplicating definitions. Since arbitrary updates to a signature can
invalidate the inversion principles used to check case expressions, we develop
a definition of signature well-formedness that ensures that extensions maintain
existing inversion principles. This definition allows different parts of a
program to extend the same signature in different ways, without conflicting
with each other. Each part can be type-checked independently, allowing separate
compilation.

Programming Languages