Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation(…)

on YouTube ↗25m

" summary

Zoo delivers a transpiler plus proof framework that translates OCaml 5 into a limited ZooLang fragment embedded via a deep embedding in Rocq, where programs get verified with Iris concurrent separation logic. It formalizes OCaml physical equality more precisely, adds atomic record fields/arrays and generative constructors to the language, and proves correctness of a subset of the standard library, Saturn lock‑free structures and Eio RCFD and persistent stores, showing the approach is practical.

AI-written summary · about

" chapters (8)

1. 0:00Zoo framework introduction
2. 3:14Zoo features overview
3. 7:58OCaml language contributions
4. 9:03Verification and case studies
5. 11:57Physical equality challenges
6. 16:41Why physical equality fails
7. 20:18Consequences of false equality
8. 23:05Generative constructors future work