A Formalization of Operads in Coq

要約

プログラミング言語内での実行の正確性について最高レベルの保証を提供するものは何ですか?
この問題に対する 1 つの答え、特に私たちの解決策は、プログラミング言語の表示セマンティクスの形式化 (存在する場合) を提供することです。
このような形式化を達成することで、プログラミング言語が構成によって正しいことを保証するためのゴールド スタンダードが提供されます。
DARPA V-SPELLS プログラムでの取り組みでは、オペラドとして知られる数学的オブジェクトを使用して、メタ言語の表示セマンティクスの基盤を提供するために取り組みました。
このオブジェクトには、小さな断片から言語を構築するのに不可欠な構成プロパティがあります。
この論文では、証明アシスタント Coq におけるオペラドの形式化について説明します。
さらに、Coq 内での定義は、Coq 内で指定されたオブジェクトがオペランドであることを証明することができます。
Coq 内でのこの作業は、V-SPELLS 内でのメタ言語開発の正式な数学的基礎を提供します。
私たちの仕事はまた、私たちの知る限りでは、ホモトピー型理論の知識がなくても複製できるモデルだけでなく、重要な自動化を備えた証明アシスタント内でのオペラドの最初の知られている形式化も提供します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google