Osiris: an Iris-based program logic for OCaml
summary
Osiris provides an Iris-based program logic inside Coq to verify OCaml modules by translating OCaml ASTs into a deep-embedded Coq representation and proving an after spec for the resulting computation. It uses Iris in Coq and a translation tool from OCaml to Coq, defines a two-step (micro + step) semantics that computes pure reductions and then small-step behavior, and uses a simp predicate to eliminate nondeterministic evaluation; currently supports modules, ADTs, tuples, records, recursion and lacks unsafe features, GC, and full language coverage.
AI-written summary · about
chapters (6)
- 0:00Osiris introduction
- 3:32Proof methodology overview
- 8:08Semantics for OCaml
- 13:25Reasoning rules
- 16:13Current state and future
- 17:40Q&A
related talks
21mLive Verification in an Interactive Proof Assistant
27mTry-Mopsa: Relational Static Analysis in Your Pocket
07h 18mFull Workshop
23mStructured diagnostics for the OCaml compiler
22mVsCoq 2, new foundations
43mOCaml at LexiFi
22mInteractive Source-to-Source Optimizations Validated using Static Resource Analysis
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...