Melocoton is a research project building a multi-language model and program verification system for OCaml, C, and their interactions through the OCaml foreign function interface.

Melocoton consists of a formal semantics of a large subset of the OCaml FFI, and a program logic to reason about the interaction of program components written in OCaml and C.

Melocoton is fully mechanized using Coq and the Iris separation logic framework.



Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, Derek Dreyer