Skeletal semantics and their interpretations
File(s)popl19main-p89-p.pdf (854.7 KB)
Published version
OA Location
Author(s)
Bodin, Martin
Gardner, Philippa
Jensen, Thomas
Schmitt, Alan
Type
Conference Paper
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.
Date Issued
2019-01-02
Date Acceptance
2018-10-09
Citation
Proceedings of the ACM on Programming Languages, 2019, 3, pp.44:1-44:31
ISSN
2475-1421
Publisher
Association for Computing Machinery
Start Page
44:1
End Page
44:31
Journal / Book Title
Proceedings of the ACM on Programming Languages
Volume
3
Copyright Statement
© 2019 Copyright held by the owner/author(s). This work is licenced under a Creative Commons Attribution-ShareAlike 4.0 International licence
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Grant Number
EP/K008528/1 - RG65358
EP/K008528/1
Source
ACM SIGPLAN Symposium on Principles of Programming Languages (POPL )
Publication Status
Published
Start Date
2019-01-13
Finish Date
2019-01-19
Coverage Spatial
Cascais, Portugal