In Web-based computing, services and clients must agree on their contract--the order of the messages to be exchanged--in order to have a successful conversation. In particular, it must be possible to decide whether the contract offered by a service is compatible with the contract accepted by a client, or whether one service can be safely replaced by another service that has a different contract.

This paper addresses these problems by introducing a subcontract relation between contracts σ and τ, so that every client that complies with the services of σ also complies with the services of τ. One might be tempted to immediately consider every service of τ as a service of σ, but the authors realize that this view leads to a dead end: central properties such as the transitivity of the subcontract relation cannot be established. Therefore, the authors adopt an idea from type theory: a process of τ can be coerced to a process of σ by a filter that removes behaviors not visible in σ.

The authors elaborate this idea into a complete theory. Their deduction system yields a subcontract checker that generates a filter between contracts or proves that no filter exists. This enjoyable paper explains the basic intuitive ideas that set the stage for the formal presentations. Although the authors do not elaborate on certain aspects, such as contracts for infinite behaviors, the theory presented in this paper builds a strong basis for further research.