Certified Derivation of Small-Step From Big-Step Skeletal Semantics
Guillaume Ambal, Sergueï Lenglet, Alan Schmitt, Camille Noûs · 2022
We present an automatic translation of a skeletal semantics written in big-step style into an equivalent structural operational semantics. This translation is implemented on top of the Necro tool, which lets us automatically generate an OCaml interpreter for the small step semantics and a Coq mechanization of both semantics. We prove the framework correct in two ways: we provide a paper proof of the core of the transformation, and we generate Coq certification scripts alongside the transformation. We illustrate the approach using a simple imperative language and show how it scales to larger languages.