Add to ORKGSkeletal semantics is a framework to describe the operational semantics of programming languages. We first 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 transformation correct in two ways: we provide a paper proof of the core of the translation, and we generate Coq certification scripts alongside the transformation. We also propose an automatic generation of a certified OCaml interpreter for any language written in skeletal semantics. To this end, we intr...