Necro ML: Generating OCaml Interpreters
summary
Necro ML generates OCaml interpreters from skel skeletal semantics and outputs modular, monad-parameterized code that preserves unspecified types and terms. A 31-line OCaml glue file instantiates module types for unspecified types, produces an interpreter that runs a factorial test yielding 3628800, and swaps monads to change nondeterminism handling (identity picks first branch, a continuation monad does backtracking). Source and examples live on GitLab and Jscale shows real JavaScript coverage.
AI-written summary · about
chapters (5)
- 0:00Introduction
- 0:46Generating Interpreters
- 2:08Operational Semantics
- 11:00Necro Tools
- 11:52Necro Applications
related talks
20mCertified Abstract Machines for Skeletal Semantics
15mType-safe generation of modules in applicative and generative styles
35mDeriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang
28mImplicit modules, a middle step towards modular implicits
29mMechanized monadic equational reasoning for ML references
24mCode Extraction from Coq to ML-like languages
23mMacro-embedding Compiler Intermediate Languages in Racket
38mDemystifying compilers by writing your own