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.

翻译：编程语言执行正确性的最高保障是什么？针对该问题，一种答案（也是我们的解决方案）是：若存在编程语言的指称语义，则为其提供形式化。实现这种形式化可为确保编程语言"构造即正确"提供黄金标准。在DARPA V-SPELLS项目中，我们致力于利用一种称为operad的数学对象为元语言的指称语义奠定基础。该对象具有组合性质，对从更小构件构建语言至关重要。本文讨论我们在证明助手Coq中对operad的形式化。此外，我们的Coq定义能够证明在Coq中指定的对象是operad。这项工作为V-SPELLS中的元语言开发提供了形式化的数学基础。据我们所知，我们的工作首次在具备强大自动化能力的证明助手中实现了operad的形式化，并提供了无需理解同伦类型理论即可复现的模型。