A Formalization of Operads in Coq
This work provides a foundational tool for formal verification in programming language design, particularly for the DARPA V-SPELLS program, but it is incremental as it builds on existing mathematical concepts.
The authors tackled the problem of ensuring correctness in programming languages by formalizing the denotational semantics of a meta-language using operads, resulting in the first known formalization of operads in the Coq proof assistant with significant automation and a replicable model without requiring Homotopy Type Theory knowledge.
What provides the highest level of assurance for correctness of execution within a programming language? One answer, and our solution in particular, to this problem is to provide a formalization for, if it exists, the denotational semantics of a programming language. Achieving such a formalization provides a gold standard for ensuring a programming language is correct-by-construction. In our effort on the DARPA V-SPELLS program, we worked to provide a foundation for the denotational semantics of a meta-language using a mathematical object known as an operad. This object has compositional properties which are vital to building languages from smaller pieces. In this paper, we discuss our formalization of an operad in the proof assistant Coq. Moreover, our definition within Coq is capable of providing proofs that objects specified within Coq are operads. This work within Coq provides a formal mathematical basis for our meta-language development within V-SPELLS. Our work also provides, to our knowledge, the first known formalization of operads within a proof assistant that has significant automation, as well as a model that can be replicated without knowledge of Homotopy Type Theory.