Skeletal Semantics and their Interpretations

Abstract : The development of mechanised language specification based on structured operational semantics, with applications to verified compilers and sound program analysis, requires huge effort. General theory and frameworks have been proposed to help with this effort. However, none of this work provides a systematic way of developing concrete and abstract semantics, connected together by a general consistency result. We introduce a skeletal semantics of a language, where each skeleton describes the complete semantic behaviour of a language construct. We define a general notion of interpretation, which provides a systematic and language-independent way of deriving semantic judgements from the skeletal semantics. We explore four generic interpretations: a simple well-formedness interpretation; a concrete interpretation; an abstract interpretation; and a constraint generator for flow-sensitive analysis. We prove general consistency results between interpretations, depending only on simple language-dependent lemmas. We illustrate our ideas using a simple While language.
Type de document :
Article dans une revue
Proceedings of the ACM on Programming Languages, ACM, In press, 44, pp.1-31. 〈10.1145/3290357〉
Liste complète des métadonnées

Littérature citée [3 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01881863
Contributeur : Alan Schmitt <>
Soumis le : vendredi 23 novembre 2018 - 09:49:10
Dernière modification le : vendredi 30 novembre 2018 - 11:20:05

Fichier

rule-format.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Martin Bodin, Philippa Gardner, Thomas Jensen, Alan Schmitt. Skeletal Semantics and their Interpretations. Proceedings of the ACM on Programming Languages, ACM, In press, 44, pp.1-31. 〈10.1145/3290357〉. 〈hal-01881863v3〉

Partager

Métriques

Consultations de la notice

300

Téléchargements de fichiers

213