Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

https://hal.inria.fr/hal-02946930
Contributor : Guillaume Ambal <>
Submitted on : Thursday, September 24, 2020 - 12:27:02 PM
Last modification on : Saturday, September 26, 2020 - 3:08:33 AM

File

RR-9363.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02946930, version 2

Citation

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⟩

Share

Metrics

Record views

30

Files downloads

92