Skeletal Semantics
body
Necro is an ecosystem written in OCaml to manipulate skeletal semantics. It is composed of the following projects.
- The Necro Library is used to parse and type skeletal semantics. It is used in most of the projects below.
- Necro Tests provides many examples of skeletal semantics.
- Necro ML is a generator of an OCaml interpreter from a skeletal semantics.
- Necro Debug is a generator of a debugger from a skeletal semantics: it runs it step by step. This can be tested on a small example here.
- Necro Coq is a generator of a Coq formalization of a natural (big-step) semantics from a skeletal semantics.
- Necro Dep generates a graph of dependencies between declared values in a skeletal semantics.