Skeletal Semantics and their Interpretations

Abstract : Many metalanguages have been proposed for writing rule-based operational semantics, in order to provide general interpreters and analysis tools. We take a different approach. We develop a metalanguage for 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 provide four generic interpretations of our skeletal semantics to yield: a simple well-formedness interpretation; a concrete interpretation; an abstract interpretation; and a constraint generator for flow-sensitive analysis. We prove general consistency results, establishing that the concrete and abstract interpretations are consistent and that any solution to the constraints generated by the constraint generator must be a correct abstract semantics.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-01881863
Contributor : Alan Schmitt <>
Submitted on : Wednesday, September 26, 2018 - 1:21:59 PM
Last modification on : Friday, September 13, 2019 - 9:48:42 AM
Long-term archiving on : Thursday, December 27, 2018 - 1:35:25 PM

File

rule-format.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01881863, version 1

Citation

Martin Bodin, Philippa Gardner, Thomas Jensen, Alan Schmitt. Skeletal Semantics and their Interpretations. 2018. ⟨hal-01881863v1⟩

Share

Metrics

Record views

356

Files downloads

27