Coq 8.5 中的范畴论
计算机科学中的逻辑
2015-05-26 v1
摘要
我们报告了在 Coq 8.5 中实现范畴论的经验。该开发的代码库可在 https://bitbucket.org/amintimany/categories/ 找到。该实现最显著地利用了 Coq 8.5 新增的特性，即记录的原始投影（primitive projections）和宇宙多态（universe polymorphism）。
引用
@article{arxiv.1505.06430,
title = {Category Theory in Coq 8.5},
author = {Amin Timany and Bart Jacobs},
journal= {arXiv preprint arXiv:1505.06430},
year = {2015}
}
备注
This is the abstract for a talk accepted for a presentation at the 7th Coq Workshop, Sophia Antipolis, France on June 26, 2015