A graded dependent type system with a usage-aware semantics
A graded dependent type system with a usage-aware semantics
复制标题
具有使用感知语义的分级依赖类型系统
DOI：
10.1145/3410265
复制
发表时间：
2021
影响因子：
--
通讯作者：
Weirich, Stephanie
中科院分区：
文献类型：
--
作者：
Choudhury, Pritam;Eades II, Harley;Eisenberg, Richard A.;Weirich, Stephanie
分级类型理论提供了一种跟踪和推理类型系统中资源使用的机制。在本文中，我们开发了格拉德，一个新的版本，这样一个分级依赖型系统，包括功能，张量积，加法和，单位类型。由于标准的操作语义是资源不可知的，我们开发了一个基于堆的操作语义，并证明了一个合理性定理，显示正确的会计资源的使用。从这个定理可以导出一些有用的性质，包括标准型可靠性定理、计算中不受无关资源的干扰以及线性资源的单指针性质。我们希望我们的工作将为在Haskell等实用编程语言中集成线性、无关和依赖类型提供基础。
Graded Type Theory provides a mechanism to track and reason about resource usage in type systems. In this paper, we develop GraD, a novel version of such a graded dependent type system that includes functions, tensor products, additive sums, and a unit type. Since standard operational semantics is resource-agnostic, we develop a heap-based operational semantics and prove a soundness theorem that shows correct accounting of resource usage. Several useful properties, including the standard type soundness theorem, non-interference of irrelevant resources in computation and single pointer property for linear resources, can be derived from this theorem. We hope that our work will provide a base for integrating linearity, irrelevance and dependent types in practical programming languages like Haskell.
登录
查看更多内容
类型推断、Haskell 和依赖类型
DOI：
--
发表时间：
2013
期刊：
影响因子：
--
作者：
Adam Gundry
通讯作者：
Adam Gundry
通过分级结合效应和协同效应
DOI：
10.1145/2951913.2951939
发表时间：
2016
期刊：
--
影响因子：
--
作者：
Gaboardi M
通讯作者：
Gaboardi M
Haskell 中依赖类型的角色
影响因子：
--
作者：
Weirich, Stephanie;Choudhury, Pritam;Voizard, Antoine;Eisenberg, Richard A.
通讯作者：
Eisenberg, Richard A.
模态类型理论中的内涵性、外延性和证明无关性
DOI：
10.1109/lics.2001.932499
发表时间：
2001
期刊：
Proceedings 16th Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
F. Pfenning
通讯作者：
F. Pfenning
使用交叉类型绑定器和子类型扩展纯类型系统的构造的隐式演算
DOI：
--
发表时间：
2001
期刊：
影响因子：
--
作者：
Alexandre Miquel
通讯作者：
Alexandre Miquel