Space-Efficient Manifest Contracts at POPL 15
I am delighted to announce that Space-Efficient Manifest Contracts will appear at POPL 2015 in Mumbai. Here's the 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.
The conference version is a slightly cut down version of my submission, focusing on the main result: eidetic λH is a space-efficient manifest contract calculus with the same operational behavior as classic λH. More discussion and intermediate results---all in a unified framework for space efficiency---can be found in the technical report on the arXiv.