Necro: the Skeleton Key to Semantics

Necro is an OCaml project born at Inria Rennes in June 2018, in relation to the research article Skeletal Semantics and their Interpretations made in collaboration between Inria Rennes and the Imperial College London. More information at http://skeletons.inria.fr/.

The goal of the project is to provide a tool to manipulate skeletal semantics, a format to represent the semantics of programming languages.

This repository only contains the main part of the project, i. e. the main library.

• For OCaml generation see https://gitlab.inria.fr/skeletons/necro-ml
• For gallina generation see https://gitlab.inria.fr/skeletons/necro-coq

See change log

Installation

Via opam

You can install necrolib via opam. It is not in the official opam repository yet, so it is necessary to first add our repository.

opam switch create necro 5.1.1
eval $(opam env)
opam repository add necro https://gitlab.inria.fr/skeletons/opam-repository.git#necro
opam install necrolib

From the sources

Dependencies

• bash
• autoconf
• OCaml (5.1.1 or greater)
• menhir
• dune
• dune-build-info
• ocamlgraph

Installation instructions

Run dune build

How to run it

The project contains a necro.cma and some .cmi files. If you installed via opam, you may use open Necro if you compile using ocamlfind. If you installed from the sources, you can find those files in the main directory.

The project also provides several executable, all defined in apps. See the README for more information

Tests and examples

Some examples of skeletal files are available in the necro-test repository.

Tools

In the tools folder, you will find a file for vim, a file for emacs, and a file for pygments. See tools/README.md for more informations

Inner workings

The implementation of the typer is described in file typer.pdf, it explains the role of most files. Some further details are available in the OCamlDoc, you may generate it by doing dune build @doc.