Nominal Formalisations of Typical SOS Proofs
Julien Narboux, Christian Urban · 2007
Structural operational semantics (SOS) provides a framework for ascribing semantics to programming languages. This is typically done by stating rules for typing judgements, small-step transitions and rules for evaluating an expression of the language. Structural inductions over expressions and inductions over inference rules are thus the most fundamental reasoning techniques employed in SOS. While the SOS-techniques are characterised in Plotkin’s seminal notes as “symbol-pushing”, programming languages nearly always contain binders and then reasoning is in fact rather subtle. We describe in this paper formalisations of typical proofs in SOS within the Isabelle proof assistant using the nominal datatype package. We show how this package eases the subtleties when reasoning about binders. Key words: structural operational semantics, proof assistants, nominal techniques, Isabelle/HOL “It is the purpose of these notes to develop a simple and direct method for specifying the semantics of programming languages. Very little is required in the way of mathematical background all that will be involved is “symbol-pushing ” of one kind or another of the sort which will already be familiar to readers with experience of either the non-numerical aspects of programming languages or else formal deductive systems of the kind employed in mathematical logic. ” — G. D. Plotkin [10, Page 19] 1