Mechanized monadic equational reasoning for ML references
summary
Extends a Coq mechanization by adding a typed store monad and a bespoke equational theory for ML references, implemented on top of the Mona library and a state-monad-transformer over option. An OCaml→Coq experimental compiler generates the examples. Introduces C_check and CR run operations, proves core laws and small proofs (cycle equality under reference creation in under ~10 lines, generalization ~16 lines), and exposes remaining gaps: freshness/GC equations are not validated by the chosen model.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:05ML type translation and monads
- 3:36Mona library
- 6:09Store monad for ML refs
- 8:48State transformers model
- 13:03Laws for ref operations
- 18:04Commuting operations
- 20:12Cyclic references proof
- 23:23CR run for equivalence
- 24:47Related work & conclusion
- 26:17Q&A
related talks
24mCode Extraction from Coq to ML-like languages
19mInterpreting OCaml GADTs into Coq
19mExtensible Metatheory Mechanization via Family Polymorphism
01h 06mVerifying a compiler through equational means
11mLocal algebraic effect theories
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
15mTowards a Coq Specification for Generalized Algebraic Datatypes in OCaml
30mA Mechanised Semantics of Erlang’s References