ATTENTION: The software behind KU ScholarWorks is being upgraded to a new version. Starting July 15th, users will not be able to log in to the system, add items, nor make any changes until the new version is in place at the end of July. Searching for articles and opening files will continue to work while the system is being updated.
If you have any questions, please contact Marianne Reed at mreed@ku.edu .
The Root Cause of Blame: Contracts for Intersection and Union Types
dc.contributor.author | Williams, Jack | |
dc.contributor.author | Morris, J. Garrett | |
dc.contributor.author | Wadler, Philip | |
dc.date.accessioned | 2018-10-26T20:03:24Z | |
dc.date.available | 2018-10-26T20:03:24Z | |
dc.date.issued | 2018-11 | |
dc.identifier.citation | Jack Williams, J. Garrett Morris, and Philip Wadler. 2018. The Root Cause of Blame: Contracts for Intersection and Union Types. Proc. ACM Program. Lang. 2, OOPSLA, Article 134 (November 2018), 29 pages. https://doi.org/10.1145/3276504 | en_US |
dc.identifier.uri | http://hdl.handle.net/1808/27076 | |
dc.description.abstract | Gradual typing has emerged as the tonic for programmers with a thirst for a blend of static and dynamic typing. Contracts provide a lightweight form of gradual typing as they can be implemented as a library, rather than requiring a gradual type system.Intersection and union types are well suited to static and dynamic languages: intersection encodes overloaded functions; union encodes uncertain data arising from branching code. We extend the untyped lambda calculus with contracts for monitoring higher-order intersection and union types, for the first time giving a uniform treatment to both. Each operator requires a single reduction rule that does not depend on the constituent types or the context of the operator.We present a new method for defining contract satisfaction based on blame behaviour. A value positively satisfies a type if applying a contract of that type can never elicit positive blame. A continuation negatively satisfies a type if applying a contract of that type can never elicit negative blame. We supplement our definition of satisfaction with a series of monitoring properties that satisfying values and continuations should have. | en_US |
dc.publisher | Association for Computing Machinery | en_US |
dc.rights | © 2018 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License. | en_US |
dc.rights.uri | https://creativecommons.org/licenses/by/4.0/ | en_US |
dc.subject | Functional languages | en_US |
dc.subject | Semantics | en_US |
dc.subject | Theory of computation | en_US |
dc.subject | Program semantics | en_US |
dc.subject | Software and its engineering | en_US |
dc.subject | Gradual typing | en_US |
dc.subject | Blame | en_US |
dc.subject | Contracts | en_US |
dc.subject | Intersection | en_US |
dc.subject | Union | en_US |
dc.title | The Root Cause of Blame: Contracts for Intersection and Union Types | en_US |
dc.type | Article | en_US |
kusw.kuauthor | Morris, J. Garrett | |
kusw.kudepartment | Electrical Engineering & Computer Science | en_US |
dc.identifier.doi | 10.1145/3276504 | en_US |
kusw.oaversion | Scholarly/refereed, publisher version | en_US |
kusw.oapolicy | This item meets KU Open Access policy criteria. | en_US |
dc.rights.accessrights | openAccess | en_US |