[PRL] [1410.2813] Space-Efficient Manifest Contracts

[Mitchell Wand]

http://arxiv.org/abs/1410.2813

Space-Efficient Manifest Contracts
Michael Greenberg <http://arxiv.org/find/cs/1/au:+Greenberg_M/0/1/0/all/0/1>
(Submitted on 10 Oct 2014)

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.
Along the way, we define a framework for space efficiency, traversing the
design space with three different space-efficient manifest calculi. We
examine the diverse correctness criteria for contract semantics; we
conclude with a coercion-based language whose contracts enjoy
(galactically) bounded, sound space consumption---they are observationally
equivalent to the standard, space-inefficient semantics.

Comments:This is an extended version of a POPL'15 paper, with a great deal
of material that does not appear in the conference paper: an exploration of
the design space with two other space-efficient calculi and complete proofs
Subjects:Programming Languages (cs.PL)Cite as:arXiv:1410.2813
<http://arxiv.org/abs/1410.2813> [cs.PL] (or arXiv:1410.2813v1
<http://arxiv.org/abs/1410.2813v1> [cs.PL] for this version)
-------------- next part --------------
HTML attachment scrubbed and removed