GSOS Formalized in Coq

Structural operational semantics provides a well known framework to describe the semantics of programming languages, lending itself to formalization in theorem provers. The formalization of syntactic SOS rule formats, which enforce some form of well-behavedness, has so far received less attention. GSOS is a rule format that enjoys the property that the operational semantics and denotational semantics, both derived from the same set of GSOS rules, are consistent. The present paper formalizes the underlying theory in the theorem prover COQ, and proves the consistency property, also known as the adequacy theorem. The inspiration for our work has been drawn from the field of bialgebraic semantics.