Unifying hybrid types and contracts Export

@inproceedings{citeulike:5820562, abstract = {Contract systems and hybrid type systems provide two alternative approaches for enforcing precisely-defined interface specifications, with complementary advantages: contract systems excel at blame assignment, whereas hybrid type systems support type-based static analysis. We unify these two approaches by demonstrating that hybrid type checking is sufficiently expressive to encode higher-order contracts with proper blame assignment. In particular, a contract obligation that enforces both sides of a contract is decomposed into two type casts that each enforce one side of the contract. This expressiveness result provides several benefits, including allowing one of these casts to be lifted to earlier in the program's execution, resulting in improved contract coverage. 1}, author = {Gronski, Jessica and Flanagan, Cormac}, booktitle = {In Eighth Symposium on Trends in Functional Programming}, citeulike-article-id = {5820562}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.123.3771}, keywords = {bulletproofing, contracts, translation, typed}, posted-at = {2009-09-22 14:44:03}, priority = {0}, title = {Unifying hybrid types and contracts}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.123.3771}, year = {2007} }

TY - CONF ID - citeulike:5820562 L3 - citeulike-article-id:5820562 N2 - Contract systems and hybrid type systems provide two alternative approaches for enforcing precisely-defined interface specifications, with complementary advantages: contract systems excel at blame assignment, whereas hybrid type systems support type-based static analysis. We unify these two approaches by demonstrating that hybrid type checking is sufficiently expressive to encode higher-order contracts with proper blame assignment. In particular, a contract obligation that enforces both sides of a contract is decomposed into two type casts that each enforce one side of the contract. This expressiveness result provides several benefits, including allowing one of these casts to be lifted to earlier in the program’s execution, resulting in improved contract coverage. 1 TI - Unifying hybrid types and contracts T2 - In Eighth Symposium on Trends in Functional Programming KW - bulletproofing KW - contracts KW - translation KW - typed AU - Gronski, Jessica AU - Flanagan, Cormac PY - 2007/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.123.3771 ER -