TY - GEN
T1 - Space-Efficient manifest contracts
AU - Greenberg, Michael
N1 - Publisher Copyright:
Copyright © 2015 by the Association for Computing Machinery, Inc. (ACM).
PY - 2015/1/14
Y1 - 2015/1/14
N2 - The standard algorithm for higher-order contract checking can lead to unbounded space consumption and can destroy tail recursion, altering a program's asymptotic space complexity. While space efficiency for gradual types-contracts mediating untyped and typed code-is well studied, sound space efficiency for manifest contracts-contracts that check stronger properties than simple types, e.g., "is a natural" instead of "is an integer"-remains an open problem. We show how to achieve sound space efficiency for manifest contracts with strong predicate contracts. The essential trick is breaking the contract checking down into coercions: structured, blame-annotated lists of checks. By carefully preventing duplicate coercions from appearing, we can restore space efficiency while keeping the same observable behavior.
AB - The standard algorithm for higher-order contract checking can lead to unbounded space consumption and can destroy tail recursion, altering a program's asymptotic space complexity. While space efficiency for gradual types-contracts mediating untyped and typed code-is well studied, sound space efficiency for manifest contracts-contracts that check stronger properties than simple types, e.g., "is a natural" instead of "is an integer"-remains an open problem. We show how to achieve sound space efficiency for manifest contracts with strong predicate contracts. The essential trick is breaking the contract checking down into coercions: structured, blame-annotated lists of checks. By carefully preventing duplicate coercions from appearing, we can restore space efficiency while keeping the same observable behavior.
KW - Coercions
KW - Contracts
KW - Function proxy
KW - Pre- And post-conditions
KW - Space efficiency
UR - http://www.scopus.com/inward/record.url?scp=84939494147&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84939494147&partnerID=8YFLogxK
U2 - 10.1145/2676726.2676967
DO - 10.1145/2676726.2676967
M3 - Conference contribution
AN - SCOPUS:84939494147
T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
SP - 181
EP - 194
BT - POPL 2015 - Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
T2 - 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015
Y2 - 12 January 2015 through 18 January 2015
ER -