Relational cost analysis for functional-imperative programs
Relational cost analysis for functional-imperative programs
复制标题
功能命令式程序的关系成本分析
DOI：
10.1145/3341696
复制
发表时间：
2019
影响因子：
--
通讯作者：
Garg, Deepak
中科院分区：
文献类型：
--
作者：
Qu, Weihao;Gaboardi, Marco;Garg, Deepak
关系成本分析旨在正式确定两个项目评估成本差异的界限。作为一种特殊情况，我们还可以使用关系成本分析来确定同一项目在两个不同输入上的评估成本差异的界限。执行关系成本分析的一种方法是使用关系类型和效果系统，该系统支持推理两个程序的两次执行之间的关系。基于这一基本思想，我们提出了一种称为 ARel 的类型和效果系统，用于推理数组操作、高阶函数命令程序的相对成本。我们方法的关键要素是一种新的轻量级类型细化规则，我们用它来跟踪两个可变数组之间的关系（差异）。这一规则与类型中内置的霍尔式三元组相结合，使我们能够表达和建立几个有趣的程序的精确相对成本，这些程序必须更新其数据。我们使用双向类型检查的思想实现了 ARel。
Relational cost analysis aims at formally establishing bounds on the difference in the evaluation costs of two programs. As a particular case, one can also use relational cost analysis to establish bounds on the difference in the evaluation cost of the same program on two different inputs. One way to perform relational cost analysis is to use a relational type-and-effect system that supports reasoning about relations between two executions of two programs.Building on this basic idea, we present a type-and-effect system, called ARel, for reasoning about the relative cost of array-manipulating, higher-order functional-imperative programs. The key ingredient of our approach is a new lightweight type refinement discipline that we use to track relations (differences) between two mutable arrays. This discipline combined with Hoare-style triples built into the types allows us to express and establish precise relative costs of several interesting programs which imperatively update their data. We have implemented ARel using ideas from bidirectional type checking.
登录
查看更多内容
随控制流变化而增加计算复杂性的类型理论
DOI：
--
发表时间：
2016
期刊：
ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
Ezgi Çiçek;Zoe Paraskevopoulou;D. Garg
通讯作者：
D. Garg
影响因子：
--
作者：
Benton, Nick;Hofmann, Martin;Nigam, Vivek
通讯作者：
Nigam, Vivek
线性相关类型和相对完整性
DOI：
10.2168/lmcs-8(4:11)2012
发表时间：
2011
期刊：
2011 IEEE 26th Annual Symposium on Logic in Computer Science
影响因子：
--
作者：
Ugo Dal Lago;Marco Gaboardi
通讯作者：
Marco Gaboardi
关系成本分析
DOI：
--
发表时间：
2017
期刊：
ACM-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
Ezgi Çiçek;G. Barthe;Marco Gaboardi;Deepak Garg;Jan Hoffmann
通讯作者：
Jan Hoffmann
DOI：
10.1145/3314221.3314603
发表时间：
2019
期刊：
Programming Language Design and Implementation (PLDI
影响因子：
--
作者：
Çiçek, Ezgi;Qu, Weihao;Barthe, Gilles;Gaboardi, Marco;Garg, Deepak
通讯作者：
Garg, Deepak