Certified Abstract Machines for Skeletal Semantics - Archive ouverte HAL Access content directly
Conference Papers Year :

Certified Abstract Machines for Skeletal Semantics

(1) , (2, 3) , (1, 4)
1
2
3
4

Abstract

Skeletal semantics is a framework to describe semantics of programming languages. We propose an automatic generation of a certified OCaml interpreter for any language written in skeletal semantics. To this end, we introduce two new interpretations, i.e., formal meanings, of skeletal semantics, in the form of non-deterministic and deterministic abstract machines. These machines are derived from the usual bigstep interpretation of skeletal semantics using functional correspondence, a standard transformation from big-step evaluators to abstract machines. All these interpretations are formalized in the Coq proof assistant and we certify their soundness. We finally use the extraction from Coq to OCaml to obtain the certified interpreter.
Fichier principal
Vignette du fichier
cpp.pdf (502.48 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-03466807 , version 1 (06-12-2021)

Identifiers

Cite

Guillaume Ambal, Sergueï Lenglet, Alan Schmitt. Certified Abstract Machines for Skeletal Semantics. CPP 2022 - 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2022, Philadelphia, United States. pp.1-13, ⟨10.1145/3497775.3503676⟩. ⟨hal-03466807⟩
250 View
222 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More