一句话：为 OCaml 的一个含效应处理器的顺序片段建立形式语义与两种程序逻辑。
本文是迈向 OCaml 形式化定义与基础程序验证环境的第一步。作者定义了 OLang——OCaml 的一个非平凡顺序片段，涵盖一等函数、普通与可扩展代数数据类型、模式匹配、引用、异常以及效应处理器。其动态语义被定义为一个单子解释器：计算在自定义单子内部表示为操作树，并配备小步语义，从而在解释器与操作语义之间建立联系。在此基础上，论文给出两种程序逻辑：一种无状态 Hoare 逻辑用于推理所谓“纯”程序，另一种基于 Iris 的分离逻辑用于推理任意程序。文章详细描述了两种逻辑的构造，并给出若干使用示例，展示了该片段在形式化验证方面的可用性。
This paper makes a first step towards a formal definition of OCaml and a foundational program verification environment for OCaml. We present a formal definition of OLang, a nontrivial sequential fragment of OCaml, which includes first-class functions, ordinary and extensible algebraic data types, pattern matching, references, exceptions, and effect handlers. 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. We define two program logics for OLang. A stateless Hoare Logic allows reasoning about so-called “pure” programs; an Iris-based Separation Logic allows reasoning about arbitrary programs. We present the construction of the two logics as well as some examples of their use.
@article{paperbot3041,
title = {Formal Semantics and Program Logics for a Fragment of OCaml},
author = {Remy Seassau and Irene Yoon and Jean-Marie Madiot and François Pottier},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {ICFP},
year = {2025},
doi = {10.1145/3747509}
}