No.050 Software Contracts for Communication, Monitoring, and Security

Manifest contract calculi are a family of statically typed
  higher-order contract calculi where contract information occurs as
  refinement types---e.g., {x:Int|0 < x} means positive integers.
  Contracts in such calculi are checked statically if possible;
  otherwise dynamically with type conversion, also called casts.  It
  is a natural idea to apply refinement types to algebraic datatypes
  because data structures are often constructed or manipulated in such
  a way as to meet certain specifications---e.g., a list constructed
  by a sorting function must be sorted.  A naive combination, however,
  leads to inefficient dynamic contract checking.

  We propose *manifest datatypes*, of which argument types of data
  constructors can be refined, with the mechanism of casts between
  different but compatible datatypes to make dynamic contract checking
  more efficient.  We formalize a contract calculus for manifest
  datatypes with a semantics and a type system and prove type
  soundness.  We also describe systematic generation of manifest
  datatype definitions from refinement types, delayed contract
  checking, and a prototype implementation using Camlp4.