Space-efficient manifest contracts

Research output: Contribution to journalArticlepeer-review

2 Scopus citations

Abstract

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.

Original languageEnglish
Pages (from-to)181-194
Number of pages14
JournalACM SIGPLAN Notices
Volume50
Issue number1
DOIs
StatePublished - Jan 2015

Keywords

  • Coercions
  • Contracts
  • Function proxy
  • Pre- and post-conditions
  • Space efficiency

Fingerprint

Dive into the research topics of 'Space-efficient manifest contracts'. Together they form a unique fingerprint.

Cite this