Skeletal Semantics

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.