Oct 122009
 

Roberto Zunino and myself have recently investigated the logical foundations of contracts in concurrent systems.  A contract is an agreement stipulated between two or more parties, which specifies the duties and the rights of the parties involved therein. We have modelled contracts as formulae in an intuitionistic logic extended with a “contractual” form of implication.  We have proved decidability of our logic via cut elimination: this allows us to mechanically infer the rights and the duties deriving from any set of contracts. We have embedded 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. We have then shown how to exploit our calculus as a tool for modelling services, the interaction of which is driven by contracts.

References

  • Massimo Bartoletti and Roberto Zunino. A calculus of contracting processes.
    To appear in LICS 2010.
    A draft is available here.
  • Massimo Bartoletti and Roberto Zunino. A calculus of contracting processes.
    Technical Report DISI-09-056, 2009.
    [pdf]
  • Massimo Bartoletti and Roberto Zunino. A logic for contracts.
    Technical Report DISI-09-034, 2009
    . [pdf]
 Posted by on 12 October 2009  Unica
credits unica.it | accessibilità Università degli Studi di Cagliari
C.F.: 80019600925 - P.I.: 00443370929
note legali | privacy

Nascondi la toolbar