Formal Component-Based Semantics

Formal Component-Based Semantics (FCBS) is a formalization of Component-Based Semantics in the Coq proof assistant. It enables the user to reason about programming language properties in a modular way.

Component-Based Semantics (CBS) describes programming languages in terms of combinations of abstract constructs. Abstract constructs have a fixed, language-independent meaning. CBS proposes the creation of an (open-ended) repository of abstract constructs, which can be freely combined to describe programming languages. The formalization is based on Modular Structural Operational Semantics (MSOS), a framework that supports the description of the semantics of the abstract constructs. Both CBS and MSOS have been developed by Peter D. Mosses.


Coq sources: fcbs-0.1.tar (build with scons), or browse at Github.

The above package includes some files of the math-classes and Heq libraries for Coq.


Ken Madlener, Sjaak Smetsers and Marko van Eekelen. Formal Component-Based Semantics.
Structural Operational Semantics 2011 (SOS 2011), held at CONCUR 2011. Electronic Proceedings in Theoretical Computer Science 62, pp. 17-29, 2011. link.