Stating and Handling Semantics with Skel and Necro

Énoncer et manipuler des sémantiques avec Skel et Necro

Louis Noizet (1) , Alan Schmitt (1)

1 CELTIQUE - Software certification with semantic analysis

We present Skel, a meta language designed to describe the semantics of programming languages, and Necro, a set of tools to manipulate said descriptions. We show how Skel, although minimal, can faithfully and formally capture informal specifications. We also show how we can use these descriptions to generate OCaml interpreters and Coq formalizations of the specified language.

Ni prezentas Skel, metalingvon fasonitan por priskribi la semantikon de programlingvoj, kaj Necro, ilaro por manipuli tiojn priskribojn. Ni montras kiel Skel, kvankam malgranda, povas fidele kaj formale kapti neformalajn specifojn. Ni ankaŭ montras kiel oni povas uzi tiojn priskribojn por naski OCaml interpretilojn kaj Coq formaladojn de la specifita lingvo.

Ce document présente Skel, un méta-langage conçu pour décrire les sémantiques de langages de programmation, et Necro, un ensemble d’outils pour manipuler lesdites descriptions. Nous montrons comment Skel, bien que minimal, peut fidèlement et formellement capturer des spécifications informelles. Nous montrons également comment ces descriptions peuvent être utiliséès pour générer des interpréteurs OCaml et des formalisations Coq du langage spécifié.

Mots clés: Skel; Necro; semantics; skeletal semantics; OCaml; Coq; formalization

Mots clés: Skel; Necro; sémantique; sémantique squelettique; OCaml; Coq; formalisation

Domaines: Langage de programmation [cs.PL]

Louis Noizet, Alan Schmitt. Stating and Handling Semantics with Skel and Necro. [Research Report] RR-9449, Inria Rennes - Bretagne Atlantique. 2022, pp.1-20. ⟨hal-03543701v1⟩