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.
Links
- Paper at OOPSLA'23
- slides of the presentation (with animations / without animations)
- Git repository
- Chat
- Johannes Hostert's master thesis (expands on the OOPLSA paper)
People
Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, Derek Dreyer