Skeletal Semantics and their Interpretations

International audienceThe development of mechanised language specification based on structured operational semantics, withapplications to verified compilers and sound program analysis, requires huge effort. General theory andframeworks have been proposed to help with this effort. However, none of this work provides a systematic wayof developing concrete and abstract semantics, connected together by a general consistency result. We introducea skeletal semantics of a language, where each skeleton describes the complete semantic behaviour of a languageconstruct. We define a general notion of interpretation, which provides a systematic and language-independentway of deriving semantic judgements from the skeletal semantics. We explore four generic interpretations: asimple well-formedness interpretation; a concrete interpretation; an abstract interpretation; and a constraintgenerator for flow-sensitive analysis. We prove general consistency results between interpretations, dependingonly on simple language-dependent lemmas. We illustrate our ideas using a simple While language