立体类型论的内部参数性
摘要：计算类型理论中联结了笛卡尔立方体类型理论的内在等价结构和内在参量性原理的定义。这一综合理论支持异态性及其关联等效性，我们将其称为相对性。我们通过分析高阶归纳类型之间的多态函数的使用来展示该理论的应用，观察立方体等同如何调整参量类型理论，以及研究立方体和参量类型理论之间的相似之处和差异，它们是密切相关的。我们还抽象出了计算解释的形式接口，并展示了它具有预层模型。
作者：Evan Cavallo and Robert Harper
论文ID：2005.11290
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22