一句话：提出首个 Esterel 等式演算，支持源码级等式重写推理程序行为，并帮助发现实现缺陷。
Esterel 广泛用于安全关键系统，其精确语义利于推理，但已有语义要么翻译为布尔电路，要么给出运行整个程序的操作语义，缺乏在源码层进行等式推理的理论。本文提出首个 Esterel 等式演算，通过一组等式重写规则刻画程序行为，使程序员可在源语言层面证明变换、重构与求值。文章用一系列示例等价展示演算的实用性，并说明该演算如何帮助发现 Esterel 实现中的错误。
The language Esterel has found success in many safety-critical applications, such as fly-by-wire systems and nuclear power plant control software. Its imperative style is natural to programmers building such systems and its precise semantics makes it work well for reasoning about programs. Existing semantics of Esterel generally fall into two categories: translation to Boolean circuits, or operational semantics that give a procedure for running a whole program. In contrast, equational theories enable reasoning about program behavior via equational rewrites at the source level. Such theories form the basis for proofs of transformations inside compilers or for program refactorings, and defining program evaluation syntactically. This paper presents the first such equational calculus for Esterel. It also illustrates the calculus’s usefulness with a series of example equivalences and discuss how it enabled us to find bugs in Esterel implementations.
@article{paperbot643,
title = {A calculus for Esterel: if can, can. if no can, no can.},
author = {Spencer P. Florence and Shu-Hung You and Jesse A. Tov and Robert Bruce Findler},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290374}
}