# A Formal Algebraic Framework for DSL Composition

arXiv: https://arxiv.org/abs/2302.00744 · HTML: https://mlsanity.com/paper/2302.00744/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 2 of its 8 references that are in the map.
- First posted on arXiv 1 Feb 2023.

## Builds on (most cited first, 2 of 2)

- [Operads for complex system design specification, analysis and synthesis](https://mlsanity.com/paper/2101.11115/) (2021)
- [Operads for Designing Systems of Systems](https://mlsanity.com/paper/2009.12647/) (2020)

## Abstract (arXiv)

We discuss a formal framework for using algebraic structures to model a meta-language that can write, compose, and provide interoperability between abstractions of DSLs. The purpose of this formal framework is to provide a verification of compositional properties of the meta-language. Throughout our paper we discuss the construction of this formal framework, as well its relation to our team's work on the DARPA V-SPELLS program via the pipeline we have developed for completing our verification tasking on V-SPELLS. We aim to give a broad overview of this verification pipeline in our paper. The pipeline can be split into four main components: the first is providing a formal model of the meta-language in Coq; the second is to give a specification in Coq of our chosen algebraic structures; third, we need to implement specific instances of our algebraic structures in Coq, as well as give a proof in Coq that this implementation is an algebraic structure according to our specification in the second step; and lastly, we need to give a proof in Coq that the formal model for the meta-language in the first step is an instance of the implementation in the third step.