Published August 2025 | Version v3
- 1. Inria Centre de Recherche de Paris
Description
This artifact is a Rocq mechanization relating to OLang, a nontrivial fragment of OCaml, which includes first-class functions, ordinary and extensible algebraic data types, pattern matching, references, exceptions, and effect handlers.
It comes in two forms, both with the same content: a QEMU image with preinstalled dependencies and a source archive file.
Both the image and the source file contain:
- the definition and formal semantics of OLang, as well as two program logics which allow users to reason about OLang programs
- a translator, which takes an OCaml program and outputs a Rocq file containing its translation into OLang
We define the dynamic semantics of OLang as a monadic interpreter. This interpreter runs atop a custom monad where computations are internally represented as trees of operations and equipped with a small-step semantics.
Our two program logics are: a stateless Hoare Logic allows reasoning about so-called "pure" programs; an Iris-based Separation Logic allows reasoning about arbitrary programs.
This work represents a first step towards a formal definition of OCaml and a foundational program verification environment for OCaml.
This artifact requires no specific hardware.