Literature Review: Smart Contract Semantics <s> Evaluation of Reviewed Formalisms <s> Abstract: Contracting is an essential aspectof doing business. Electronic contracting uses telecommunications and artificial intelligence to improve contracting processes by streamlining red tape enforcing legal correctness. To do this, the underlying conceptual structures of contracts and contracting must be carefully understood. A logic model is presented that emphasizes temporal, deontic and performative aspects of contracting. <s> BIB001 </s> Literature Review: Smart Contract Semantics <s> Evaluation of Reviewed Formalisms <s> This paper presents a coordination model for expressing behaviour in an extended enterprise. Our model is unified because it enables the same style of expressions for describing behaviour/structure in a self-contained enterprise and for describing cross-enterprise behaviour/structure. This model can support a broad range of modelling activities but the specific focus of this paper is on deriving the key elements of a domain language primarily targeted at expressing and monitoring behavioural conditions stated in business contracts. We also show how business contracts serve as a unifying mechanism for describing interactions in the extended enterprise. <s> BIB002 </s> Literature Review: Smart Contract Semantics <s> Evaluation of Reviewed Formalisms <s> We present a declarative language for compositional specification of contracts governing the exchange of resources. It extends Eber and Peyton Jones’s declarative language for specifying financial contracts (Jones et al. in The Fun of Programming. 2003) to the exchange of money, goods and services amongst multiple parties and complements McCarthy’s Resources, Events and Agents (REA) accounting model (McCarthy in Account Rev. LVII(3), 554–578, 1982) with a view- independent formal contract model that supports definition of user-defined contracts, automatic monitoring under execution and user-definable analysis of their state before, during and after execution. We provide several realistic examples of commercial contracts and their analyses. A variety of (real) contracts can be expressed in such a fashion as to support their integration, management and analysis in an operational environment that registers events. The language design is driven by both domain considerations and semantic language design methods: a contract denotes a set of traces of events, each of which is an alternative way of concluding the contract successfully, which gives rise to a CSP-style (Brooker et al. in J.ACM 31(3), 560–599, 1984; Hoare in Communicating Sequential Processes, 1985) denotational semantics. The denotational semantics drives the development of a sound and complete small-step operational semantics, where a partially executed contract is represented as a (full) contract that represents the remaining contractual commitments. This operational semantics is then systematically refined in two stages to an instrumented operational semantics that reflects the bookkeeping practice of identifying the specific contractual commitment a particular event matches at the time the event occurs, as opposed to delaying this matching until the contract is concluded. <s> BIB003 </s> Literature Review: Smart Contract Semantics <s> Evaluation of Reviewed Formalisms <s> In this paper we propose a formal language for writing electronic contracts, based on the deontic notions of obligation, permission, and prohibition. We take an ought-to-do approach, where deontic operators are applied to actions instead of state-of-affairs. We propose an extension of the µ-calculus in order to capture the intuitive meaning of the deontic notions and to express concurrent actions. We provide a translation of the contract language into the logic, the semantics of which faithfully captures the meaning of obligation, permission and prohibition. We also show how our language captures most of the intuitive desirable properties of electronic contracts, as well as how it avoids most of the classical paradoxes of deontic logic. We finally show its applicability on a contract example. <s> BIB004
Hvitved  BIB002 , And is Andersen et al BIB003 . and Pri is Prisacariu and Schneider BIB004 As noted by Vanca  , the formalisms proposed by Andersen et al. BIB003 . and Prisacariu et al. BIB004 are the only ones that consist of complete formal models, languages, and semantics. However, there is no proof that these formalisms can correctly replicate the semantics of contracts. Additionally, these formalisms fail to meet requirement 7: support for instantaneous and continuous actions. This would be render them unsuitable for modelling derivatives contracts as these contracts typically prescribe some long term, continuous obligations. While it does not satisfy all of the requirements, Lee's framework BIB001 is the next best option. The law firm King & Wood Mallesons published a report in collaboration with ISDA which highlights some further requirements that are specific to the finance industry  . Namely, smart contracts would have to be constructed with strict adherence to regulatory standards with an emphasis on safety and transparency, while still meeting the performance expectations of their users. The report also identifies a benefit of working in the domain of financial derivatives: the ISDA Common Domain Model (CDM). The CDM is a dictionary of events and actions that can occur during the lifecycle of a derivatives contract. The data is accessible in an unambiguous and machine interpretable way, and can therefore be integrated into a formal model for derivatives contracts. In the next section, different aspects of Lee's framework are presented and assessed. The analysis is done by looking at how the formalism deals with the deontic, temporal, and operational aspects of contracts. Additionally, this analysis looks at how the separability problem makes it difficult to develop formalisms to exclusively model each individual aspect.