Operad 在 Coq 中的形式化
范畴论
2023-03-17 v1 计算与语言
编程语言
摘要
什么能为编程语言内的执行正确性提供最高级别的保证?对这一问题的一个答案,也是我们的具体解决方案,是为编程语言的指称语义(若存在)提供形式化。实现这样一种形式化为确保编程语言按构造正确提供了黄金标准。在DARPA V-SPELLS项目的努力下,我们致力于使用一种称为operad的数学对象为某元语言的指称语义提供基础。该对象具有组合性质,这对于从较小片段构建语言至关重要。在本文中,我们讨论在证明辅助工具Coq中对operad的形式化。此外,我们在Coq中的定义能够给出Coq内所指定对象是operad的证明。该Coq内的工作为我们在V-SPELLS中的元语言开发提供了形式化的数学基础。据我们所知,我们的工作还提供了首个在证明辅助工具中对operad的已知形式化,其具有显著的自动化能力,并且是一个无需同伦类型论知识即可复现的模型。
引用
@article{arxiv.2303.08894,
title = {A Formalization of Operads in Coq},
author = {Zachary Flores and Angelo Taranto and Eric Bond and Yakir Forman},
journal= {arXiv preprint arXiv:2303.08894},
year = {2023}
}
备注
Repository for code to follow shortly