Formal Component-Based Semantics
Ken Madlener (Radboud University Nijmegen, The Netherlands), Sjaak, Smetsers (Radboud University Nijmegen, The Netherlands), Marko van Eekelen, (Radboud University Nijmegen, The Netherlands)
TL;DR
This paper formalizes Component-Based Semantics in Coq, leveraging Modular SOS, dependent types, and type classes to enable modular meta-theoretic reasoning and proofs, demonstrated through a determinism proof of a mini-language.
Contribution
It provides the first formalization of Component-Based Semantics in Coq using Modular SOS, dependent types, and type classes for modular meta-theoretic reasoning.
Findings
Successful formalization of Component-Based Semantics in Coq
Development of a modular proof of determinism for a mini-language
Demonstration of the approach's effectiveness for modular meta-theoretic reasoning
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.