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 (Latest revision fixing some typos)
- Git repository
- Chat
- Johannes Hostert's master thesis (expands on the OOPLSA paper)
- Gurvan Debaussart's internship report on adding local roots
- Valeran Maytie's internship report on adding exceptions
Talks
- Talk at OOPSLA'23 by Johannes Hostert (slides with animations / without animations)
- Keynote at CoqPL'24 by Armaël Guéneau (video / slides)
People
Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, Derek Dreyer