Osiris: An Iris-Based Program Logic for OCaml

Explore a conference talk that introduces Osiris, a project aimed at helping OCaml developers verify their code using Separation Logic. Delve into the details of this Iris-based program logic for OCaml, which currently supports a subset of OCaml language features including modules, mutual recursion, ADTs, tuples, and records. Learn about the project's goals to extend support for most OCaml language features and its use of Iris, a Coq framework for Separation Logic. Discover how Osiris provides an Iris instantiation with a presentation of OCaml semantics, enabling reasoning on realistic OCaml programs. Understand the translation tool that converts OCaml files to Coq files, and the process of verifying OCaml programs using Osiris. Gain insights into the project's potential impact on OCaml development and code verification practices.

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