Bounded Linear Types in a Resource Semiring
Bounded Linear Types in a Resource Semiring
复制标题
资源半环中的有界线性类型
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Alex I. Smith
中科院分区：
文献类型：
--
作者：
D. Ghica;Alex I. Smith
有界线性类型已被证明对于函数式编程语言中的自动化资源分析和控制非常有用。在本文中，我们介绍了关于可以在半环中建模的资源的一般概念的有界线性类型规则。对于这个类型系统，我们提供了一个通用的类型推断过程，由半环方程理论的决策过程参数化，以及一个连贯的分类语义。这可能是用于资源敏感编译的有用的类型理论和指称框架，并且它代表了几种现有类型系统的概括。作为一个重要的实例，在硬件编译的推动下，我们提出了一个复杂的新应用程序，用于计算和控制具有本地存储的无递归高阶函数编程语言的执行时间。
Bounded linear types have proved to be useful for automated resource analysis and control in functional programming languages. In this paper we introduce a bounded linear typing discipline on a general notion of resource which can be modeled in a semiring. For this type system we provide both a general type-inference procedure, parameterized by the decision procedure of the semiring equational theory, and a coherent categorical semantics. This could be a useful type-theoretic and denotational framework for resource-sensitive compilation, and it represents a generalization of several existing type systems. As a non-trivial instance, motivated by hardware compilation, we present a complex new application to calculating and controlling timing of execution in a recursion-free higher-order functional programming language with local store.