Formal Component-Based Semantics
| Autor: | Madlener, Ken, Smetsers, Sjaak, van Eekelen, Marko |
|---|---|
| Rok vydání: | 2011 |
| Předmět: | |
| Zdroj: | EPTCS 62, 2011, pp. 17-29 |
| Druh dokumentu: | Working Paper |
| DOI: | 10.4204/EPTCS.62.2 |
| Popis: | 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. Comment: In Proceedings SOS 2011, arXiv:1108.2796 |
| Databáze: | arXiv |
| Externí odkaz: |
|