一句话：提出 ARel 类型与效应系统，用类型精化与 Hoare 式三元组追踪可变数组关系，分析函数式-命令式程序相对代价。
关系代价分析旨在形式化地界定两个程序求值代价之差，也可用于比较同一程序在两个输入上的代价差异。已有方法多用关系类型与效应系统，但难以处理会命令式更新可变数组的高阶程序。本文提出 ARel：一个面向数组操作的高阶函数式-命令式程序的关系类型与效应系统。其关键是一种轻量级类型精化机制，用于追踪两个可变数组之间的关系（差异），并与内建于类型中的 Hoare 式三元组结合，从而表达和证明若干会命令式更新数据的有趣程序的精确相对代价。作者基于双向类型检查实现了 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.
@article{paperbot615,
title = {Relational cost analysis for functional-imperative programs},
author = {Weihao Qu and Marco Gaboardi and Deepak Garg},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {ICFP},
year = {2019},
doi = {10.1145/3341696}
}