Melocoton: A Program Logic for Verified Interoperability Between OCaml and C
summary
Melocoton claims the first formal semantics of the OCaml FFI and the first multi‑language program logic that reasons about OCaml and C interactions, implemented as a mechanized Coq development on top of Iris (using transfinite Iris). It implements per‑location root conversion rules backed by a ghost heap to let individual OCaml points‑to convert to C block representations and back, models garbage collection, callbacks, and pointer arithmetic, and provides evaluated reusable artifacts and case studies showing the approach works.
AI-written summary · about
chapters (9)
- 0:00Melocoton introduction
- 2:07OCaml and C interoperability
- 5:34Language locality vs interaction
- 8:00Glue code semantics challenges
- 12:34Why naive separation logic fails
- 13:47Ghost heaps for language barriers
- 15:33Multilanguage verification challenges
- 16:14Melocoton summary in Iris
- 16:35Q&A: Integration with verifiers
related talks
01h 02mMelocoton: A Program Logic for Verified Interoperability Between OCaml and C (I...
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
11mMorello Cerise: proving secure encapsulation (work in progress)
40mRetrofitting Concurrency – Lessons from the Engine Room
40mFormal semantics for multi-language programs
01h 07mThe Cogent and Dargent approach to facilitating verified software development
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
01h 04mCoq's vibrant ecosystem for verification engineering