Skeletal Semantics


Skeletal Semantics consist of Skel, a meta language designed to describe the semantics of programming languages, and Necro, a set of tools to manipulate said descriptions. Skel, although minimal, can faithfully and formally capture many forms of specification, from inductive rules to complex algorithmic descriptions. Necro includes the generator of OCaml interpreters and Coq formalizations from semantics written in Skel.