News‎ > ‎

Vicious circles in contracts and in logic

posted Jan 21, 2015, 5:18 AM by Massimo Bartoletti   [ updated Jan 21, 2015, 5:18 AM ]
Upcoming paper (to appear in Science of Computer Programming)

M. Bartoletti, T. Cimoli, P. Di Giamberardino, and R. Zunino

Abstract. Contracts are formal promises on the future interactions of participants, which describe the causal dependencies among their actions. An inherent feature of contracts is that such dependencies may be circular: for instance, a buyer promises to pay for an item if the seller promises to ship it, and vice versa. We establish a bridge between two formal models for contracts, one based on games over event structures, and the other one on Propositional Contract Logic. In particular, we show that winning strategies in the game-theoretic model correspond to proofs in the logic.