Vicious circles in contracts and in logic

• We relate Propositional Contract Logic (PCL) with games over event structures.
• We characterize agreement in a class of games in terms of provability in PCL.
• We show that prudent plays in games correspond to proof traces in PCL.
• We show that winning strategies in the games correspond to proofs in PCL.

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.