Coq 中的 HoTT 形式化：依赖图与 ML4PG
计算机科学中的逻辑
2014-03-12 v1
摘要
本说明是对 Bas Spitter 于 2014 年 2 月 28 日关于 ML4PG 的邮件的回复：“我们（实际上是 Jason）正在向我们的 HoTT 库添加依赖图：https://github.com/HoTT/HoTT/wiki 我似乎记得，寻找依赖图是阻碍机器学习在 Coq 中应用的主要障碍。然而，您似乎在此方面取得了进展。您使用的是哪种工具？https://anne.pacalet.fr/dev/dpdgraph/ ？还是其他工具？在 HoTT 库上使用您的 ML4PG 是否容易？”本说明解释了如何在 HoTT 库中使用 ML4PG，以及 ML4PG 与 Coq 中可用的两种依赖图之间的关系。
引用
@article{arxiv.1403.2531,
title = {HoTT formalisation in Coq: Dependency Graphs \& ML4PG},
author = {Jónathan Heras and Ekaterina Komendantskaya},
journal= {arXiv preprint arXiv:1403.2531},
year = {2014}
}