Formal Component-Based Semantics
Logic in Computer Science
2011-08-17 v1
Abstract
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.
Keywords
Cite
@article{arxiv.1108.3125,
title = {Formal Component-Based Semantics},
author = {Ken Madlener and Sjaak Smetsers and Marko van Eekelen},
journal= {arXiv preprint arXiv:1108.3125},
year = {2011}
}
Comments
In Proceedings SOS 2011, arXiv:1108.2796