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 Tex generates text or LaTeX description of the rules of a skeletal semantics.
  • Necro Dep generates a graph of dependencies between declared values in a skeletal semantics.