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

The standard algorithm for higher-order contract checking

can lead to unbounded space consumption and can destroy tail
recursion. In this work, we show how to achieve space efficiency for
contract checking. Working in a manifest context, we define a family
of languages: classic λH, which is inefficient; forgetful λH, which is
efficient but skips some checks; and heedful λH, which is efficient
but may change blame labels. We show first that if classic λH produces
a value, then so does forgetful λH (but not vice versa); we then show
that classic and heedful λH yield identical values, but possibly
differing blame labels.