idris-ct：一个用于在 Idris 中开展范畴论的库
计算机科学中的逻辑
2020-09-16 v2 范畴论
摘要
我们介绍 idris-ct，一个提供范畴概念的可验证类型定义的 Idris 库。idris-ct 力求成为学术界与工业界之间的桥梁，既服务于希望在实际环境中实现并尝试其想法的范畴论研究者，也服务于重视以范畴论进行形式化的企业与工程师：它受为定理证明开发的类似库启发，但保持非常实用，面向业务中的软件生产。尽管如此，依赖类型的使用使得范畴概念的形式正确实现成为可能，从而能够对软件性质提供保证。
引用
@article{arxiv.1912.06191,
title = {idris-ct: A Library to do Category Theory in Idris},
author = {Fabrizio Genovese and Alex Gryzlov and Jelle Herold and Andre Knispel and Marco Perone and Erik Post and André Videla},
journal= {arXiv preprint arXiv:1912.06191},
year = {2020}
}
备注
In Proceedings ACT 2019, arXiv:2009.06334