Deriving Abstract Interpreters from Skeletal Semantics

This paper describes a methodology for defining an executable abstract interpreter from a formal description of the semantics of a programming language. Our approach is based on Skeletal Semantics and an abstract interpretation of its semantic meta-language. The correctness of the derived abstract i...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2023-09
Main Authors: Jensen, Thomas, Rébiscoul, Vincent, Schmitt, Alan
Format: Article
Language:English
Subjects:
Interpreters
Programming languages
Semantics
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper describes a methodology for defining an executable abstract interpreter from a formal description of the semantics of a programming language. Our approach is based on Skeletal Semantics and an abstract interpretation of its semantic meta-language. The correctness of the derived abstract interpretation can be established by compositionality provided that correctness properties of the core language-specific constructs are established. We illustrate the genericness of our method by defining a Value Analysis for a small imperative language based on its skeletal semantics.
ISSN:2331-8422
DOI:10.48550/arxiv.2309.07298