New and improved: Space-Efficient Manifest Contracts
I have a new and much improved draft of my work on Space-Efficient Manifest Contracts. 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. We define a framework for space efficiency, traversing the design space with three different space-efficient manifest calculi. Along the way, we examine the diverse correctness criteria for contract semantics; we conclude with a language whose contracts enjoy (galactically) bounded, sound space consumption---they are observationally equivalent to the standard, space-inefficient semantics.
Update: it was accepted to POPL'15!