Melocoton: A Program Logic for Verified Interoperability Between OCaml and C (I...
summary
Melocoton gives a verified way to link OCaml and C: it supplies the first formal semantics of the OCaml FFI and a program logic that reasons end-to-end about OCaml code, C glue, and their boundary. Verification reuses existing ML/C logics, models runtime transitions that convert the high‑level OCaml heap to a block heap for glue code, and proves view reconciliation rules plus an adequacy theorem. The development is mechanized in Coq on top of Iris, handles callbacks, custom blocks, and uses angelic nondeterminism for block→value extraction.
AI-written summary · about
chapters (17)
- 0:00Welcome
- 1:03Motivation for multilanguage verification
- 3:52OCaml-C interoperability challenges
- 5:20OCaml-C mixed code example
- 8:31Iris and Melocoton approach
- 11:40Language-local reasoning in Melocoton
- 14:28Reusing single-language logics
- 15:13External calls and interface assumptions
- 21:28Bridging memory models
- 25:28Dual-heap operational semantics
- 30:26Memory view reconciliation rules
- 35:43C semantics in Coq
- 40:44Linking languages and wrapping
- 43:55Program triples and correctness
- 46:47Adequacy theorem and safety
- 47:07Melocoton summary and future work
- 51:01Q&A
related talks
18mMelocoton: A Program Logic for Verified Interoperability Between OCaml and C
21mVerified Extraction from Coq to OCaml
01h 06mVerifying a compiler through equational means
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
26mAn Invitation to OCaml
01h 05mMuch Still to Do in Compiler Verification (A Perspective from the CakeML Project)- 01h 06mVerifying a compiler through equational means
23mVellvm: Formalizing the Informal