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

https://hal.inria.fr/hal-03466807
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

File

cpp.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03466807, version 1

Citation

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

Share

Metrics

Les métriques sont temporairement indisponibles