类型系统λω×≤

为研究高阶子类型的范畴论语义模型 ,区分了带高阶子类型的类型系统中的各种上下文 ,并简化其中的受限全称量词类型引入规则 ,而提出了类型系统λω×≤ .文章介绍该类型系统有关类别 (Kind)、算子 (Operator)、项 (Term)的规则 ,及其与建立范畴论语义模型有关的结构性质 .