一句话：提出依赖精化类型与效应系统及不动点逻辑演绎方法，以组合化验证高阶函数式程序的时序性质。
高阶函数式程序的时序性质验证长期面临组合性与自动化之间的权衡。本文提出一种依赖精化类型与效应系统，其中依赖时序效应是事件序列和程序值上的不动点逻辑谓词，可突破以往非依赖时序效应的限制，并把程序各部分的时序行为概括为效应后组合。作者进一步将类型检查与可类型化归约为求解一阶不动点逻辑约束，并给出新的演绎系统：借助不变式与良基关系进行推理，将同时含最小与最大不动点的公式化归为基于谓词的推理。其理论结果表明良类型程序满足给定时序性质，并为自动化验证提供算法途径。
Existing approaches to temporal verification of higher-order functional programs have either sacrificed compositionality in favor of achieving automation or vice-versa. In this paper we present a dependent-refinement type & effect system to ensure that well-typed programs satisfy given temporal properties, and also give an algorithmic approach---based on deductive reasoning over a fixpoint logic---to typing in this system. The first contribution is a novel type-and-effect system capable of expressing dependent temporal effects, which are fixpoint logic predicates on event sequences and program values, extending beyond the (non-dependent) temporal effects used in recent proposals. Temporal effects facilitate compositional reasoning whereby the temporal behavior of program parts are summarized as effects and combined to form those of the larger parts. As a second contribution, we show that type checking and typability for the type system can be reduced to solving first-order fixpoint logic constraints. Finally, we present a novel deductive system for solving such constraints. The deductive system consists of rules for reasoning via invariants and well-founded relations, and is able to reduce formulas containing both least and greatest fixpoints to predicate-based reasoning.
DOI 原文 ·
@inproceedings{paperbot4372,
title = {A Fixpoint Logic and Dependent Effects for Temporal Property Verification},
author = {Yoji Nanjo and Hiroshi Unno and Eric Koskinen and Tachio Terauchi},
booktitle = {LICS},
year = {2018},
doi = {10.1145/3209108.3209204}
}