Deriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang
summary
Derives a runnable Erlang interpreter by extracting Gallina functions from a Coq mechanised semantics of Core Erlang into Haskell, applying three extraction optimizations: strict substitution, replacing maps/sets with stdlib equivalents, and simplified substitutions. Adds a scheduler to make nondeterministic semantics deterministic and builds a computation-graph explorer that enumerates interleavings for a 100-process concurrent example. Reports that even after optimisations 96% of runtime is spent on structural substitutions, so the interpreter is correct and usable but slow.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 1:10Core Erlang semantics foundation
- 2:15Sequential semantics layer
- 5:30Actor model in Core Erlang
- 7:15Process local semantics
- 10:34Interprocess nondeterminism
- 16:56Rocq proof assistant implementation
- 17:38Executable functions from definitions
- 21:41Node style interpreter interface
- 22:43Haskell extraction and optimizations
- 25:13Efficient substitution and maps
- 26:19Scheduler and cycles
- 28:03Erlang ecosystem integration
- 29:11Parallel execution explorer
- 31:02Pros and cons
- 33:33Performance challenges
- 34:15Closing remarks
related talks
21mSynthesizing Formal Semantics from Executable Interpreters
18mA native interpreter for Elm
23mVellvm: Formalizing the Informal
16mCompiling Symbolic Execution with Staging and Algebraic Effects
24mTransforming Big-Step to Small-Step Semantics Using Interpreter Specialisation
44mA Few Improvements to Erlang
01h 38mGHC Core Optimisations
15mA Principled Approach to REPL Interpreters