一句话：提出未类型化传值 λ 演算的稳定关系指称语义，并据此导出高阶程序模块化关系分析。
本文针对高阶程序缺乏兼具语义基础与模块化能力的关系分析这一问题，为未类型化传值 λ 演算提出一种新的指称语义：项被解释为替换与值之间的二元稳定关系，并满足单调性。该语义刻画高阶程序的输入-输出行为，相对于操作语义被证明是可靠且完备的，同时可呈现为一种程序逻辑。作者遵循抽象解释原则，将该指称语义用作收集语义，推导出面向高阶程序的模块化关系分析；该分析能推断程序参数与结果之间的相等关系，从而为函数式程序提供一种 frame condition。评估以形式化语义性质与推导分析为主。
We present a novel denotational semantics for the untyped call-by-value λ-calculus, where terms are interpreted as stable relations , i.e. as binary relations between substitutions and values, enjoying a monotonicity property. The denotation captures the input-output behaviour of higher-order programs, and is proved sound and complete with respect to the operational semantics. The definition also admits a presentation as a program logic. Following the principles of abstract interpretation, we use our denotational semantics as a collecting semantics to derive a modular relational analysis for higher-order programs. The analysis infers equalities between the arguments of a program and its result—a form of frame condition for functional programs.
@article{MontaguJ20,
title = {Stable relations and abstract interpretation of higher-order programs},
author = {Benoît Montagu and Thomas Jensen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {ICFP},
year = {2020},
doi = {10.1145/3409001}
}