Pure type systems with subtyping

Abstract

We extend the framework of Pure Type Systems with subtyping, as found in Fω≤ This leads to a concise description of many existing systems with subtyping, and also to some new interesting systems. We develop the meta-theory for this framework, including Subject Reduction and Minimal Typing. The main problem was how to formulate the rules of the framework in such a way that we avoid circularities between theory about typing and theory about subtyping. We solve this problem by a simple but rigorous design decision: the subtyping rules do not depend on the typing rules.