Skip to Main content Skip to Navigation

Automatic Transformation of a Big-Step Skeletal Semantics into Small-Step

Guillaume Ambal 1 Alan Schmitt 1 Sergueï Lenglet 2
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
2 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : 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.
Document type :
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Guillaume Ambal Connect in order to contact the contributor
Submitted on : Thursday, September 24, 2020 - 12:27:02 PM
Last modification on : Tuesday, October 19, 2021 - 11:04:35 AM


Files produced by the author(s)


  • HAL Id : hal-02946930, version 2


Guillaume Ambal, Alan Schmitt, Sergueï Lenglet. Automatic Transformation of a Big-Step Skeletal Semantics into Small-Step. [Research Report] RR-9363, Inria Rennes - Bretagne Atlantique. 2020. ⟨hal-02946930v2⟩



Record views


Files downloads