Osiris: towards formal semantics and reasoning for OCaml
I will describe work in progress on Osiris, an attempt to equip a nontrivial fragment of OCaml with a formal semantics and with an interactive program verification environment, hosted inside the Rocq proof assistant. Our semantics is hybrid: it takes the form of a monadic interpreter, defined on top of…
