We propose a formal theory of contract-based computing. 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, which combines features from concurrent constraints and calculi for multiparty sessions, while subsuming several idioms for concurrency.
|Titolo:||A calculus of contracting processes|
|Data di pubblicazione:||2010|
|Tipologia:||4.1 Contributo in Atti di convegno|