Certified Abstract Machines for Skeletal Semantics
summary
Automatic generation produces a certified OCaml interpreter from any language written in skeletal semantics by deriving two semantics: a relation-style non-deterministic abstract machine and an executable deterministic abstract machine that implements backtracking via failure continuations. Both machines come from CPS and functionalization of the existing big‑step semantics, are formalized and proven sound in Coq, and the deterministic machine is extracted to OCaml (slower than the unverified ML generator; JS support is nearly complete).
AI-written summary · about
chapters (8)
- 0:00Start
- 0:17Skeletal Semantics
- 5:13Mutually Defined Skeletons
- 9:23Deterministic Semantics
- 10:38Backtracking
- 13:50Summary
- 16:57Replacing the Current Interpreter
- 19:01Support for Monads
related talks
36mFlexible Instruction-Set Semantics via Abstract Monads
46mMechanizing Abstract Interpretation
16mAutomatically Deriving Control-Flow Graph Generators from Operational Semantics
18mCompiling with Abstract Interpretation
36mAbstract Machines for Good
09mRetargeting an Abstract Interpreter for a New Language by Partial Evaluation (Short Paper)
26mStatically Resolvable Ambiguity
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures