A Calculus of Contracting Processes

We propose a formal theory for contract-based computing. A contract is an agreement stipulated between two or more parties, which specifies the duties and the rights of the parties involved therein. We model contracts as formulae in an intuitionistic logic extended with a contractual" form of implication. Decidability holds for our logic: this allows us to mechanically infer the rights and the duties deriving from any set of contracts. We embed our logic in a core calculus of contracting processes