A Mechanised Semantics of Erlang’s References
summary
Extends Core Erlang semantics with unique references by encoding evaluation contexts into numbers and mechanised in Rocq. Uses stdpp’s gtree to get an injective mapping and proves injectivity with a ~1000+ line Rocq proof. Only two semantic rules change, and a lemma shows map inserts do not overwrite because references differ. The encoding works for sequential termination and compiler label reuse, but it violates the core frame-stack independence property and therefore requires major redesign or a fallback to a counter-based model.
AI-written summary · about
chapters (10)
- 0:00Mechanised semantics intro
- 2:35Why formal verification matters
- 4:47Erlang references importance
- 9:28Core Erlang semantics quick
- 14:03Formalizing references challenges
- 16:52Injective encoding explained
- 22:40Practical use demo
- 25:37References limitations future
- 28:29Summary
- 29:11Q&A
related talks
29mMechanized monadic equational reasoning for ML references
51mElpi: rule-based meta-languge for Rocq
30mComputation-Tree Semantics: An Algorithmic Approach to Structurally Defined Relations
21mAdhesive Category Theory for Graph Rewriting in Rocq
15mImplementing parametricity in Rocq-ELPI
21mNested Inductive Types for Rocq and Lean
35mDeriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang
27mLightweight Semantics Engineering with Redex