Abstract: The standard formulation of bounded quantification, system F sub, is difficult to work with and lacks important syntactic properties, such as decidability. More tractable variants have been studied, but those studied so far either exclude significant classes of useful programs or lack a compelling semantics. We propose here a simple variant of F sub that ameliorates these difficulties. It has a natural semantic interpretation, enjoys a number of important properties that fail in F sub, and includes all of the programming examples for which F sub has been used in practice.
An extended abstract of this paper has been presented in the 21st Annual Symposium on Principles of Programming Languages. Portland, January 1994. It appears in the proceedings on pages 151--162.
Report (PostScript file) (270 Kbyes)