一句话：为同步块图编译器给出函数式流语义，并重述其端到端正确性定理。
同步块图语言通常被形式化为定义流函数的方程不动点。本文将这一方法应用于一个已在交互式定理证明器中验证的编译器，从而能够重新陈述其端到端正确性定理：若程序被接受且无运行时错误，则生成代码保持其输入/输出行为。在函数式语义中，必须刻画包括错误在内的所有可能行为。作者证明，静态类型与依赖分析可以正确排除除逻辑和算术运算符错误之外的所有错误。其定义补充了已有形式化，尤其针对 reset 算符给出了语义，该算符本身有用，也是高级控制结构的基础。
Synchronous block-diagram languages have long been formalized as fixpoints of equations defining stream functions. We apply this approach to a compiler verified in an interactive theorem prover, allowing us to restate its end-to-end correctness theorem: if a program is accepted and has no runtime errors, its input/output behavior is preserved in the generated code. In a functional semantics, it is necessary to model all possible behaviors, including erroneous ones. We show that static typing and dependency analyses correctly rule out all errors except those arising from logical and arithmetic operators. Our definitions supplement existing formal ones, especially for the reset operator, which is both useful in itself and a basis of advanced control structures.
DOI 原文 ·
@inproceedings{paperbot8665,
title = {Functional Stream Semantics for a Synchronous Block-Diagram Compiler},
author = {Timothy Bourke and Paul Jeanmaire and Marc Pouzet},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00052}
}