Formal Component-Based Semantics

Details Formal Component-Based Semantics Formal Component-Based Semantics

2011-08-16

arxiv.org/abs/1108.3125v1

EPTCS 62, 2011, pp. 17-29

Computer Science

Logic in Computer Science

In Proceedings SOS 2011, arXiv:1108.2796

Scientific paper

10.4204/EPTCS.62.2

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.

Affiliated with

Also associated with

No associations

Rating

Formal Component-Based Semantics does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Formal Component-Based Semantics, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Formal Component-Based Semantics will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-194561