I just submitted a paper to POPL 2014; it’s called Space-Efficient Manifest Contracts. Here’s the abstract:
Gradual types mediate the interaction between dynamic and simple types, offering an easy transition from scripts to programs; gradual types allow programmers to evolve prototype scripts into fully fledged, deployable programs. Similarly, contracts and refinement types mediate the interaction between simple types and more precise types, offering an easy transition from programs to robust, verified programs. A full-spectrum language with both gradual and refinement types offers low-level support for the development of programs throughout their lifecycle, from prototype script to verified program.
One attractive formulation of languages with gradual or refinement types uses casts to represent the runtime checks necessary for type changes (from dynamic to simple types, and from simple types to refinement types). Briefly, a cast ⟨T1⇒T2⟩ e takes a term e from type T1 to T2, possibly wrapping or tagging e in the process—or even failing, if e doesn’t meet the criteria of the type T2. Casts are attractive because they offer a unified view of changes in type, have straightforward operational semantics, and enjoy an interesting and fruitful relationship with subtyping.
One longstanding problem with casts is space efficiency: casts in their naive formulation can consume unbounded amounts of space at runtime both through excessive wrapping as well as through tail-recursion-breaking stack growth. Prior work offers space-efficient solutions exclusively in the domain of gradual types. In this paper, we define a new full-spectrum language that is (a) more expressive than prior languages, and (b) space efficient. We are the first to obtain space-efficient refinement types. Our approach to space efficiency is based on the coercion calculi of Herman et al. and Henglein’s work, though our explicitly enumerated canonical coercions and our straightforward merge operator are a novel approach to coercions with a simpler theory. We show that space efficiency avoids some checks, failing and diverging less often than naive calculi—but the two are otherwise operationally equivalent.
(Yes, I know that reviewing is double blind. But as the FAQ clearly states, double-blind review isn’t meant to hinder communication of results.)