该文提出带高阶子类型的多态类型系统λω×<,≤>,它是[Cro193]的类型系统λω×的扩充,为一般算子引入了子类型关系,并结合多态性使用了受限量词类型,与已有的各种系统F的扩充相比,其特点是区分了各种上下文,使得整个类型系统在逻辑上更严谨,也可更好地研究其语义模型.该文详细研究了类型系统λω×<,≤>的各种结构性质.该文提出λω×<,≤>fibration作为高阶子类型的语义模型,其核心是引入了带序范畴及其插入子的概念,从而将λω×<,≤>fibration基范畴的射之间的关系与全范畴的对象之间关系结合在一起,给出了一般算子之间子类型关系的语义解释,解决了在[CL91]中所说的子类型关系的通用范畴论模型问题.该文的λω×<,≤>fibration结合了[Jaco95]中定义的subtyping fibration和[Phoa92b]中提出的包含射的优点,完整地给出了受限量词的范畴论语义解释,并很好地解释了一般算子之间子类型关系以及有关子类型关系的结构性质,完整地给出了已证明项的语义模型,也给出了有关已证明项的各种结构性质规则的语义解释,证明了该模型对于已证明项的等式理论的合理性.