Content area
Modern contract systems generalize run-time assertions on Boolean expressions to higher-order functions and beyond, equipping programmers with a lightweight tool for specifying and monitoring the behavior of programs. To date, researchers have studied the theory of contract systems in every little detail, from the design of expressive notations for contracts to the correct enforcement of contracts for complex programming language constructs, and even to the asymptotic behavior of the contract system.
Although each paper contributes unique insight to the study of contract systems, researchers are bound to define custom contract calculi in order to formulate their desired metatheoretic properties. Each new contract calculus may include additional annotations that track necessary invariants for proving the metatheoretic property and custom evaluation rules of the contracts. As a result, the literature contains a large number of similar but subtly different contract calculi which require a considerable amount of repeated labor.
I address the problem with a novel transition-system-based representation of higher-order contracts. The new representation allows for building connections between a contract system and its proof invariants, and further permits the reuse of metatheories. Specifically, the transition-system representation is based on a parameterized calculus which monitors higher-order values with proxies and generates parameter-determined transition events. The calculus has a fixed base language and a predetermined monitoring strategy, but the annotations that the proxies carry are parameterized. Consequently, extra invariants needed for proving metaproperties can be encoded as custom transition events generated by the proxies, and the collection of all events naturally forms a transition system. With such transition systems, the metaproperties manifest themselves as various transition structures and hence metatheories can be reused by relating different transition systems with homomorphisms.
In this dissertation, I make three contributions based on the transition-system representation of contracts. First, I present the monitor calculus and its transition-system-based metatheory. Through the monitor calculus, I formulate properties of contract systems as particular transition structures of transition systems. Second, I apply the new representation to contract systems in the literature to construct a collection of reusable metatheories for contracts, including Findler and Felleisen’s higher-order contract system, its blame tracking mechanism, and Greenberg’s space-efficient contracts. Last, I mechanize the monitor calculus together with its metatheory and applications in Agda for the modular development of the metatheory of contracts.
