Space-Efficient Manifest Contracts
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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 14, 2015
- Source ID
- 10.1145/2775051.2676967
Entities
People
- Michael Greenberg
Organizations
- Defense Advanced Research Projects Agency
- National Science Foundation
- Princeton University