多语言程序逻辑
Multi-language Program Logics
- Institute of Science and Technology Austria (ISTA)（奥地利科学技术学院）
- MPI-SWS（马克斯·普朗克计算机系统研究所）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文提出 Hotpot，首个多语言程序逻辑框架，支持跨语言推理、规范重用及高阶跨语言调用，基于 Iris 和 DimSum 在 Rocq Prover 中机械化实现。
AI中文摘要：
现实世界中的程序很少用单一语言编写：例如，C 程序调用汇编例程，而像 OCaml 这样的高级语言与低级 C 库链接。然而，程序逻辑——模块化程序验证最成功的技术之一——几乎只针对单语言程序。我们提出了 Hotpot，这是第一个用于构建多语言程序逻辑的框架。Hotpot 支持对具有异构共享状态视图的语言进行独立于编译的跨语言推理。Hotpot 基于四个关键思想：抽象调用来指定对未知函数的调用，通道和切换模态在程序逻辑内部在语言之间移动，通过通道统一整合细化推理，以及交换以在不同语言的分离开逻辑断言之间进行转换。我们证明了 Hotpot 允许跨不同语言的实现重用规范，支持高阶跨语言函数调用的推理，并与已验证的编译集成。Hotpot 构建在 Iris 和 DimSum 之上，并在 Rocq Prover 中机械化。
英文摘要：
Real-world programs are rarely written in a single language: For example, C programs call assembly routines, and high-level languages like OCaml link with low-level C libraries. Yet program logics---one of the most successful techniques for modular program verification---almost exclusively target single-language programs. We present Hotpot, the first framework for building multi-language program logics. Hotpot enables compilation-independent, cross-language reasoning about languages with heterogeneous views of shared state. Hotpot rests on four key ideas: abstract calls to specify calls to unknown functions, lanes and the switching modality to move between languages inside the program logic, uniform integration of refinement reasoning via lanes, and exchanges to translate between separation logic assertions of different languages. We demonstrate that Hotpot allows reusing specifications across implementations in different languages, supports reasoning about higher-order cross-language function calls, and integrates with verified compilation. Hotpot is built on top of Iris and DimSum and mechanized in the Rocq Prover.
