一句话：提出类型-效应系统 ARel，借助跟踪可变数组关系的类型精化，形式化推导函数式-命令式程序间的相对求值成本界。
关系成本分析旨在形式化地界定两个程序求值成本之差，也可用于推理同一程序在不同输入下的成本差异。本文面向操作可变数组的高阶函数式-命令式程序，提出类型-效应系统 ARel。其核心是一种轻量级类型精化机制，用于追踪两个可变数组之间的差（关系）；该机制与内建于类型中的 Hoare 式三元组相结合，使系统能够表达并证明若干在命令式更新数据的程序的精确相对成本。作者基于双向类型检查实现了 ARel，展示了该方法进行精细成本推理的可行性。
Abstract 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 (the difference in the evaluation 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 that imperatively update their data. We have implemented ARel using ideas from bidirectional type checking.