一句话：提出骨架语义，用统一解释从语言构造的语义骨架系统导出具体/抽象语义及一致性结果。
基于结构化操作语义的机械化语言规范开发成本很高，且已有理论框架难以系统连接具体与抽象语义。本文提出语言的骨架语义：每个骨架完整描述一个语言构造的语义行为。作者定义通用的解释概念，以语言无关的方式从骨架语义导出语义判断，并研究四种解释：良构性解释、具体解释、抽象解释，以及面向流敏感分析的约束生成器。核心结果是证明不同解释之间的一般一致性，只需依赖简单的语言相关引理。以简单 While 语言为例展示该方法。
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.
@article{paperbot661,
title = {Skeletal semantics and their interpretations},
author = {Martin Bodin and Philippa Gardner and Thomas Jensen and Alan Schmitt},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290357}
}