Category Theory in Coq 8.5

Category Theory in Coq 8.5
复制标题

Coq 8.5 中的范畴论

DOI：
--
复制
发表时间：
2015
期刊：
International Conference on Formal Structures for Computation and Deduction
影响因子：
--
通讯作者：
B. Jacobs
B. Jacobs
中科院分区：
--
文献类型：
--
作者：
Amin Timany;B. Jacobs

文献摘要

被引文献

相似文献

我们报告了我们在Coq8.5中实现范畴理论的经验。这个开发的资源库可以在这个HTTPS URL中找到。这个实现最值得注意的是利用了Coq8.5中的新特性、记录的原语投影和全局多态。
We report on our experience implementing category theory in Coq 8.5. The repository of this development can be found at this https URL This implementation most notably makes use of features, primitive projections for records and universe polymorphism that are new to Coq 8.5.