一句话：提出去中心化的多语言语义与验证框架，各语言可独立定义、通过事件与组合子组合，并在 Coq 中验证跨语言编译器。
现有多语言程序验证工作虽已能组合式地验证复杂编译器，但通常对多语言程序施加全局限制：固定源语言、固定语言集合、固定内存模型或固定互操作语义。本文提出 DimSum，一种去中心化的多语言语义与验证方法，并在 Coq 证明助手中实现。去中心化意味着各语言可作为独立模块、经由事件相互通信而被单独定义与推理，同时在需要时又能通过组合子库进行组合与翻译。作者将 DimSum 应用于三个语言：带抽象内存模型与函数调用的高层命令式语言 Rec、带具体内存模型、任意跳转与系统调用的底层汇编语言 Asm，以及数学规约语言 Spec。评估包含两个案例研究：一个扩展 Rec 指针比较支持的 Asm 库，以及一个用 Asm 为 Rec 编写的协程库；两者都说明，尽管 Asm 库的行为无法在 Rec 中语法可表达，DimSum 仍能将其抽象为 Rec 层规约。此外还验证了一个从 Rec 到 Asm 的优化多趟编译器，证明其与这些 Asm 库兼容。
Prior work on multi-language program verification has achieved impressive results, including the compositional verification of complex compilers. But the existing approaches to this problem impose a variety of restrictions on the overall structure of multi-language programs (e.g. fixing the source language, fixing the set of involved languages, fixing the memory model, or fixing the semantics of interoperation). In this paper, we explore the problem of how to avoid such global restrictions. Concretely, we present DimSum : a new, decentralized approach to multi-language semantics and verification, which we have implemented in the Coq proof assistant. Decentralization means that we can define and reason about languages independently from each other (as independent modules communicating via events), but also combine and translate between them when necessary (via a library of combinators). We apply DimSum to a high-level imperative language Rec (with an abstract memory model and function calls), a low-level assembly language Asm (with a concrete memory model, arbitrary jumps, and syscalls), and a mathematical specification language Spec. We evaluate DimSum on two case studies: an Asm library extending Rec with support for pointer comparison, and a coroutine library for Rec written in Asm. In both cases, we show how DimSum allows the Asm libraries to be abstracted to Rec-level specifications, despite the behavior of the Asm libraries not being syntactically expressible in Rec itself. We also verify an optimizing multi-pass compiler from Rec to Asm, showing that it is compatible with these Asm libraries.
@article{paperbot2090,
title = {DimSum: A Decentralized Approach to Multi-language Semantics and Verification},
author = {Michael Sammler and Simon Spies and Youngju Song and Emanuele D'Osualdo and Robbert Krebbers and Deepak Garg and Derek Dreyer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571220}
}