一句话：首个形式化 OCaml FFI 语义并验证 OCaml/C 互操作的多语言程序逻辑，已在 Coq 中机器化。
现有程序逻辑大多假设程序完全由单一语言写成，但实际软件常由不同语言组件通过 FFI 互操作，因而缺乏多语言验证基础。本文提出 Melocoton，一个针对 OCaml、C 及其通过 OCaml FFI 交互的多语言程序验证系统。它给出了 OCaml FFI 大子集的第一个形式语义（此前仅有手册中的自然语言描述），并构建了首个用于推理 OCaml 与 C 组件交互的程序逻辑。Melocoton 在 Coq 中基于 Iris 分离逻辑框架完全机器化，为多语言程序验证迈出第一步。
In recent years, there has been tremendous progress on developing program logics for verifying the correctness of programs in a rich and diverse array of languages. Thus far, however, such logics have assumed that programs are written entirely in a single programming language. In practice, this assumption rarely holds since programs are often composed of components written in different programming languages, which interact with one another via some kind of foreign function interface (FFI). In this paper, we take the first steps towards the goal of developing program logics for multi-language verification. Specifically, we present Melocoton, a multi-language program verification system for reasoning about OCaml, C, and their interactions through the OCaml FFI. Melocoton consists of the first formal semantics of (a large subset of) the OCaml FFI—previously only described in prose in the OCaml manual—as well as the first program logic to reason about the interactions of program components written in OCaml and C. Melocoton is fully mechanized in Coq on top of the Iris separation logic framework.
@article{paperbot1850,
title = {Melocoton: A Program Logic for Verified Interoperability Between OCaml and C},
author = {Armaël Guéneau and Johannes Hostert and Simon Spies and Michael Sammler and Lars Birkedal and Derek Dreyer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622823}
}