Transformation automatique d’une sémantique squelettique grand-pas en sémantique petit-pas
Guillaume Ambal, Alan Schmitt, Sergueï Lenglet · HAL (Le Centre pour la Communication Scientifique Directe) · 2020
We present an automatic translation of a skeletal semantics written in big-step styleinto an equivalent semantics in small-step. This translation is implemented on top of the Necrotool, which lets us automatically generate an OCaml interpreter for the small step semantics and Coq mechanization of both semantics. We generate Coq certification scripts along side the transformation. We illustrate the approach using imperative language and show how it scales to larger languages.