Formal Component-Based Semantics

Ken Madlener
(Radboud University Nijmegen, The Netherlands)
Sjaak Smetsers
(Radboud University Nijmegen, The Netherlands)
Marko van Eekelen
(Radboud University Nijmegen, The Netherlands)

One of the proposed solutions for improving the scalability of semantics of programming languages is Component-Based Semantics, introduced by Peter D. Mosses. It is expected that this framework can also be used effectively for modular meta theoretic reasoning. This paper presents a formalization of Component-Based Semantics in the theorem prover Coq. It is based on Modular SOS, a variant of SOS, and makes essential use of dependent types, while profiting from type classes. This formalization constitutes a contribution towards modular meta theoretic formalizations in theorem provers. As a small example, a modular proof of determinism of a mini-language is developed.

In M.A. Reniers and P. Sobocinski: Proceedings Eight Workshop on Structural Operational Semantics 2011 (SOS 2011), Aachen, Germany, 5th September 2011, Electronic Proceedings in Theoretical Computer Science 62, pp. 17–29.
Published: 13th August 2011.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: