BSML is a pure functional library for the multi-paradigm language OCaml. BSML embodies the principles of the Bulk Synchronous Parallel (BSP) model, a model of scalable parallel computing. We propose a formalization of BSML primitives with WhyML, the specification language of Why3 and specify and prove the correctness of most of the BSML standard library. Finally, we develop and verify the correctness of a small BSML application.

翻译：BSML是一个用于多范式语言OCaml的纯函数式库。BSML体现了可扩展并行计算模型——批量同步并行（BSP）的原则。我们使用Why3的规范语言WhyML对BSML原语进行形式化，并规范及证明了BSML标准库中大部分功能的正确性。最后，我们开发并验证了一个小型BSML应用的正确性。