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

Explore a groundbreaking 18-minute conference talk from OOPSLA2 2023 that introduces Melocoton, a pioneering program verification system for reasoning about OCaml, C, and their interactions through the OCaml Foreign Function Interface (FFI). Delve into the first formal semantics of a large subset of the OCaml FFI and the innovative program logic developed to reason about multi-language program components. Learn how Melocoton addresses the challenge of verifying programs composed of different programming languages, a common scenario in practical software development. Discover the system's implementation in Coq using the Iris separation logic framework, and understand its potential impact on multi-language verification. Gain insights into foreign-function interfaces, program logics, multi-language semantics, garbage collection, and advanced concepts like angelic non-determinism and transfinite step-indexing.