Even in statically typed languages it is useful to have certain
  invariants checked dynamically.  Findler and Felleisen gave an
  algorithm for dynamically checking expressive higher-order types
  called contracts.  They did not, however, give a semantics of
  contracts.  The lack of a semantics makes it impossible to define
  and prove soundness and completeness of the checking algorithm.
  (Given a semantics, a sound checker never reports violations that do
  not exist under that semantics; a complete checker is---in
  principle---able to find violations when violations exist.)
  
  Ideally, a semantics should capture what programmers intuitively
  feel is the meaning of a contract or otherwise clearly point out
  where intuition does not match reality.
  
  In this paper we give an interpretation of contracts for which we
  prove the Findler-Felleisen algorithm sound and (under reasonable
  assumptions) complete.  While our semantics mostly matches
  intuition, it also exposes a problem with predicate contracts
  where an arguably more intuitive interpretation than ours would
  render the checking algorithm unsound.  In our semantics we have to
  make use of a notion of safety (which we define in the paper)
  to avoid unsoundness.
  
  We are able to eliminate the ``leakage'' of safety into the
  semantics by changing the language, replacing the original version
  of unrestricted predicate contracts with a restricted form.
  The corresponding loss in expressive power can be recovered by
  making safety explicit as a contract.  This can be done either in
  ad-hoc fashion or by including general recursive contracts.
  The addition of recursive contracts has far-reaching implications,
  deeply affecting the formulation of our model and requiring
  different techniques for proving soundness.