Agda泛代数库，第一部分：基础
计算机科学中的逻辑
2021-04-21 v3 逻辑
摘要
Agda泛代数库(UALib)是我们使用Agda编程语言与证明辅助工具，在依赖类型论中形式化泛代数基础所开发的一个类型与程序（定理与证明）库。UALib包含了来自一般代数与等式逻辑的大量定义、定理和证明，其中包括许多展示归纳类型与依赖类型在表示和推理关系、代数结构及等式理论方面威力的示例。在本文中，我们讨论该库所构建的逻辑基础，并描述库的前13个模块中定义的类型。我们特别关注从类型论或数学基础视角看最为有趣或最具挑战性的库的部分。
引用
@article{arxiv.2103.05581,
title = {The Agda Universal Algebra Library, Part 1: Foundation},
author = {William DeMeo},
journal= {arXiv preprint arXiv:2103.05581},
year = {2021}
}
备注
32 pages + references