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.

Paper

Ken Madlener and Sjaak Smetsers. GSOS Formalized in Coq (preprint).
7th International Symposium on Theoretical Aspects of Software Engineering (TASE 2013), IEEE, pp. 199-206, 2013.

Download

Coq sources: adequacy.tar.

Requires
Building instructions