Melocoton: A Program Logic for Verified Interoperability Between OCaml and C

Explore a groundbreaking program verification system for multi-language reasoning in this invited talk from CoqPL'24. Delve into Melocoton, a pioneering framework designed to verify the correctness of programs composed of both OCaml and C components interacting through OCaml's Foreign Function Interface (FFI). Discover the first formal semantics of a substantial subset of the OCaml FFI, previously only available in prose documentation. Learn about the innovative program logic developed to reason about interactions between OCaml and C program components. Gain insights into the full mechanization of Melocoton in Coq, built upon the Iris separation logic framework. Understand the significance of this work in addressing the challenges of verifying programs written in multiple languages, a common scenario in practical software development.