论文标题
依赖改进类型系统的一般语义构建，绝对
General Semantic Construction of Dependent Refinement Type Systems, Categorically
论文作者
论文摘要
改进类型是配备有谓词的类型，这些谓词指定了基本功能语言的前提和后条件。我们提出了从基础类型系统和谓词逻辑中的依赖细化类型系统的一般语义构造，即，从给定的（基础）封闭的理解类别和谓词逻辑的封闭理解类别的提升构建。我们提供了足够的条件来提升从依赖产品，依赖性总和，计算效应以及从基础类型系统到改进类型系统的递归的结构。我们通过将语义提供给改进类型系统并证明合理性来证明我们的构建的用法。
Refinement types are types equipped with predicates that specify preconditions and postconditions of underlying functional languages. We propose a general semantic construction of dependent refinement type systems from underlying type systems and predicate logic, that is, a construction of liftings of closed comprehension categories from given (underlying) closed comprehension categories and posetal fibrations for predicate logic. We give sufficient conditions to lift structures such as dependent products, dependent sums, computational effects, and recursion from the underlying type systems to refinement type systems. We demonstrate the usage of our construction by giving semantics to a refinement type system and proving soundness.
