Formal Semantics and Program Logics for a Fragment of OCaml
summary
Defines OLang, a sequential OCaml fragment with first-class functions, extensible ADTs, pattern matching, references, exceptions and effect handlers, and gives a concrete semantics: a layered monadic interpreter running on a custom micro monad whose computations are trees with a small‑step relation. Two logics are built: a stateless Hoare logic for pure code and an Iris‑based Separation Logic for impure code. The Coq/RoCK development extracts to OCaml and its semantics is validated against compiler behavior; concurrency and typed modules are work in progress.
AI-written summary · about