Énoncer et manipuler des sémantiques avec Skel et Necro
Noizet, Louis, Alan Schmitt · HAL (Le Centre pour la Communication Scientifique Directe) · 2022
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.