范畴依赖加细类型系统的一般语义构造
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
