Formal Component-Based Semantics

Formal Component-Based Semantics

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...

Full description

Bibliographic Details
Main Authors: Ken Madlener, Sjaak Smetsers, Marko van Eekelen
Format: Article
Language:English
Published: Open Publishing Association 2011-08-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1108.3125v1
id doaj-811c7b0a92d94eaf824429e6989a46d8
record_format Article
spelling doaj-811c7b0a92d94eaf824429e6989a46d82020-11-24T21:53:36ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802011-08-0162Proc. SOS 2011172910.4204/EPTCS.62.2Formal Component-Based SemanticsKen MadlenerSjaak SmetsersMarko van EekelenOne 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.http://arxiv.org/pdf/1108.3125v1
collection DOAJ
language English
format Article
sources DOAJ
author Ken Madlener
Sjaak Smetsers
Marko van Eekelen
spellingShingle Ken Madlener
Sjaak Smetsers
Marko van Eekelen
Formal Component-Based Semantics
Electronic Proceedings in Theoretical Computer Science
author_facet Ken Madlener
Sjaak Smetsers
Marko van Eekelen
author_sort Ken Madlener
title Formal Component-Based Semantics
title_short Formal Component-Based Semantics
title_full Formal Component-Based Semantics
title_fullStr Formal Component-Based Semantics
title_full_unstemmed Formal Component-Based Semantics
title_sort formal component-based semantics
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2011-08-01
description 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.
url http://arxiv.org/pdf/1108.3125v1
work_keys_str_mv AT kenmadlener formalcomponentbasedsemantics
AT sjaaksmetsers formalcomponentbasedsemantics
AT markovaneekelen formalcomponentbasedsemantics
_version_ 1725871155846316032

Similar Items