Skip to Main content Skip to Navigation
Conference papers

Certified Abstract Machines for Skeletal Semantics

Guillaume Ambal 1 Sergueï Lenglet 2 Alan Schmitt 1
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 : 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.
Document type :
Conference papers
Complete list of metadata
Contributor : Sergueï Lenglet Connect in order to contact the contributor
Submitted on : Monday, December 6, 2021 - 11:14:43 AM
Last modification on : Tuesday, January 4, 2022 - 6:34:55 AM


Files produced by the author(s)


  • HAL Id : hal-03466807, version 1


Guillaume Ambal, Sergueï Lenglet, Alan Schmitt. Certified Abstract Machines for Skeletal Semantics. Certified Programs and Proofs, Jan 2022, Philadelphia, United States. ⟨hal-03466807⟩



Les métriques sont temporairement indisponibles