Type refinements allow invariants about algebraic datatypes to be expressed through the type system. We present a small functional language and type system that elegantly combines datasort refinements (commonly called refinement types) and dependent index refinements, so that one can specify invariants using whatever refinement is most suitable. Our type system has intersections (novel in the presence of index refinements) and restricted dependent products; we believe ML-style references and polymorphism could be added easily. As an example, we show how the type system cleanly captures several representation invariants of red-black trees.

35 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu