Automatic Transformation of a Big-Step Skeletal Semantics into Small-Step - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2020

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

Transformation automatique d’une sémantique squelettique grand-pas en sémantique petit-pas

(1) , (1) , (2)
1
2

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.
Nous présentons une transformation automatique d’une sémantique squelettique écrite en style grand-pas vers une sémantique équivalent en style petit-pas. Cette transformation est implémentée dans l’outil Necro, ce qui nous permet de générer automatiquement un interpréteur Ocaml pour la sémantique petit-pas ainsi qu’une formalisation Coq des deux sémantiques. Nous générons un script de certification Coq en parallèle de la transformation. Nous illustrons notre approche sur un langage impératif simple.
Fichier principal
Vignette du fichier
RR-9363.pdf (789.29 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02946930 , version 1 (23-09-2020)
hal-02946930 , version 2 (24-09-2020)

Identifiers

  • HAL Id : hal-02946930 , version 2

Cite

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⟩
150 View
168 Download

Share

Gmail Facebook Twitter LinkedIn More