[OCaML'23] Osiris: an Iris-based program logic for OCaml

[OCaML'23] Osiris: an Iris-based program logic for OCaml Arnaud Daby-Seesaram, François Pottier, Armaël Guéneau Osiris is a project that aims to help OCaml developers verify their code using Separation Logic. The project is still young: we currently only support a subset of the features of the OCaml language, including modules, mutual recursion, ADTs, tuples and records. Ultimately, we would like to extend Osiris to support most features of the OCaml language. Iris is a Coq framework for Separation Logic with support for expressive ghost states. It is often used to define program logics and can be parameterized by a programming language — usually described by its small-steps semantics. Most Iris instantiations target ML-like languages, each focusing on a specific purpose and lacking support of programming features such as records or ADTs. Osiris contains an Iris instantiation with a presentation of the semantics of OCaml, in order to reason on realistic OCaml programs. Osiris provide