Guéneau, A., Hostert, J., Spies, S., Sammler, M., Birkedal, L., & Dreyer, D. (2023). Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. Proceedings of the ACM on Programming Languages, 7(OOPSLA2):, pp. 716-744. doi:10.1145/3622823.