A theory of type qualifiers

We describe a framework for adding type qualifiers to a language. Type qual ifiers encode a simple but highly useful form of subtyping. Our framework e xtends standard type rules to model the how of qualifiers through a program , where each qualifier or set of qualifiers comes with additional rules tha t capture its semantics. Our framework allows types to be polymorphic in th e type qualifiers. We present a const-inference system for C as an example application of the framework. We show that for a set of real C programs, ma ny more consts can be used than are actually present in the original code.