Skeletal semantics and their interpretations

File Description SizeFormat 
popl19main-p89-p.pdfPublished version854.7 kBAdobe PDFView/Open
Title: Skeletal semantics and their interpretations
Authors: Bodin, M
Gardner, P
Jensen, T
Schmitt, A
Item Type: Journal Article
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.
Issue Date: 2-Jan-2019
Date of Acceptance: 9-Oct-2018
ISSN: 2475-1421
Publisher: Association for Computing Machinery
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/Funder: Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Funder's Grant Number: EP/K008528/1 - RG65358
Publication Status: Published
Open Access location:
Article Number: No. 44
Appears in Collections:Faculty of Engineering

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

Creative Commonsx