A theory of agreements and protection

In this thesis we propose a theory of contracts. Contracts are modelled as interacting processes with an explicit association of obligations and objectives. Obligations are specified using event structures. In this model we formalise two fundamental notions of contracts, namely agreement and protection. These notions arise naturally by interpreting contracts as multi-player concurrent games. A participant agrees on a contract if she has a strategy to reach her objectives (or to make another participant sanctionable for a violation), whatever the moves of her counterparts. A participant is protected by a contract when she has a strategy to defend herself in all possible contexts, even in those where she has not reached an agreement. When obligations are represented using classical event structures, we show that agreement and protection mutually exclude each other for a wide class of contracts. To reconcile agreement with protection we propose a novel formalism for modelling contractual obligations: event structures with circular causality. We study this model from a foundational perspective, and we relate it with classical event structures. Using this model, we show how to construct contracts which guarantee both agreement and protection. We relate our contract model with Propositional Contract Logic, by establishing a correspondence between provability in the logic and the notions of agreement and strategies. This is a first step towards reducing the gap between two main paradigms for modelling contracts, that is the one which interprets them as interactive systems, and the one based on logic.