A Formal Algebraic Framework for DSL Composition

TL;DR

This paper presents a formal algebraic framework for modeling, composing, and verifying domain-specific languages (DSLs) using Coq, with applications demonstrated in the DARPA V-SPELLS program.

Contribution

It introduces a formal verification pipeline in Coq for algebraic structures underlying a meta-language for DSL composition.

Findings

Developed a formal Coq model of the meta-language.

Created a specification and implementation of algebraic structures in Coq.

Proved the correctness and interoperability of DSL abstractions within the framework.

Abstract

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.