proceeding Papers A Calculus of Contracting Processes


Abstract

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.



Paper Details

Authors

M. Bartoletti,  R. Zunino

Publication

Logic in Computer Science (LICS)

Language

English
.