You are here
Invited Talk: Provenance and Higher-Order Software Contracts
Website Maintenance Alert
Due to scheduled maintenance, the USENIX website will not be available on Tuesday, December 17, from 10:00 am to 2:00 pm Pacific Daylight Time (UTC -7). We apologize for the inconvenience.
If you are trying to register for Enigma 2020, please complete your registration before or after this time period.
Speaker: Christos Dimoulas, Northeastern University
Provenance information plays a critical role in judging whether the semantics of software contracts is correct. Higher-order software contracts dynamically check whether objects and functions meet the interface specifications of a component. When an object or a function fails to live up to a specification, the contract system must pinpoint the guilty party. Equipped with this blame information, a software engineer can narrow down the search for the violation—if it is correct. Provenance offers a way, based on the origin and history of the values that contracts check, to reason about the correctness of blame assignment and the effectiveness of contracts. Thus provenance provides the key element for evaluating the semantics of software contracts.
In this talk, I will introduce software contracts and the problems of checking higher-order contracts. I will present two distinct attempts to assign a semantics to contract checking in this world, and I will then demonstrate the shortcomings of both. These failures motivate the search for a formal compass for contract system designers. With semantic provenance information, we found such a compass that helped us explain why the proposed semantics failed to be useful and that guided the design of a new semantics, which is now implemented in the Racket contract system.