idris-ct: a library to do category theory in Idris. (English) Zbl 07453982

Baez, John (ed.) et al., Proceedings of the applied category theory 2019, ACT 2019, University of Oxford, UK, July 15–19, 2019. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 323, 246-254 (2020).
Summary: We introduce idris-ct, a Idris library providing verified type definitions of categorical concepts. idris-ct strives to be a bridge between academy and industry, catering both to category theorists who want to implement and try their ideas in a practical environment and to businesses and engineers who care about formalization with category theory: It is inspired by similar libraries developed for theorem proving but remains very practical, being aimed at software production in business. Nevertheless, the use of dependent types allows for a formally correct implementation of categorical concepts, so that guarantees can be made on software properties.
For the entire collection see [Zbl 1466.68006].


68-XX Computer science
18-XX Category theory; homological algebra
Full Text: arXiv Link


[1] agda. Agda Homepage. URL: https://github.com/agda/agda (cit. on p. 247).
[2] Paolo Baldan, Roberto Bruni, and Ugo Montanari. “Pre-Nets, Read Arcs and Unfolding: A Func-torial Presentation”. In: Recent Trends in Algebraic Development Techniques. Ed. by Martin Wirs-ing, Dirk Pattinson, and Rolf Hennicker. Vol. 2755. Springer Berlin Heidelberg, 2003, pp. 145-164. DOI: 10.1007/978-3-540-40020-2_8. (Visited on Apr. 20, 2019) (cit. on p. 246).
[3] Edwin Brady. Edwinb/Blodwen. URL: https://github.com/edwinb/Blodwen (cit. on p. 247).
[4] Edwin Brady. “Idris, a General-Purpose Dependently Typed Programming Language: Design and Implementation”. In: Journal of Functional Programming 23.05 (Sept. 15, 2013), pp. 552-593. DOI: 10.1017/S095679681300018X (cit. on p. 247). · Zbl 1295.68059
[5] Edwin Brady. Type-Driven Development With Idris. Manning Publications, 2017. 480 pp. (cit. on p. 247).
[6] Conexus Team. CQL Homepage. URL: http://cql.conexus.ai/index.php (cit. on p. 247).
[7] Simon Fowler and Edwin Brady. “Dependent Types for Safe and Secure Web Programming”. In: Proceedings of the 25th Symposium on Implementation and Application of Functional Languages -IFL ’13. The 25th Symposium. ACM Press, 2014, pp. 49-60. DOI: 10.1145/2620678.2620683 (cit. on p. 247).
[8] Free Software Foundation. GNU Affero General Public License Version 3 (AGPL-3.0). 2007. URL: https://www.gnu.org/licenses/agpl-3.0.en.html (cit. on p. 247).
[9] Fabrizio Genovese and Jelle Herold. “Executions in (Semi-)Integer Petri Nets Are Compact Closed Categories”. In: Electronic Proceedings in Theoretical Computer Science 287 (Jan. 31, 2019), pp. 127-144. DOI: 10.4204/EPTCS.287.7 (cit. on p. 246).
[10] Fabrizio Genovese et al. “Computational Petri Nets: Adjunctions Considered Harmful”. In: arXiv (Apr. 29, 2019). arXiv: 1904.12974 [cs, math]. (Visited on May 2, 2019) (cit. on p. 246).
[11] Jason Gross, Adam Chlipala, and David I. Spivak. “Experience Implementing a Performant Category-Theory Library in Coq”. In: Interactive Theorem Proving. Ed. by Gerwin Klein and Ruben Gam-boa. Red. by David Hutchison et al. Vol. 8558. Springer International Publishing, 2014, pp. 275-291. DOI: 10.1007/978-3-319-08970-6_18. (Visited on Apr. 23, 2019) (cit. on p. 247). · Zbl 1416.68163
[12] Haskell.org. Haskell Homepage. URL: https://www.haskell.org/ (cit. on p. 247).
[13] Dan Licata. Running Circles Around (In) Your Proof Assistant; or, Quotients That Compute. 2011. URL: https : / / homotopytypetheory. org / 2011 / 04 / 23 / running -circles -around -in -your -proof -assistant/ (cit. on p. 251).
[14] Saunders MacLane. Categories for the Working Mathematician. Vol. 5. Springer New York, 1978. DOI: 10.1007/978-1-4757-4721-8. (Visited on May 5, 2018) (cit. on pp. 247, 249).
[15] Brian McKenna and Nathan Dots. Puffnfresh/Iridium. URL: https://github.com/puffnfresh/iridium (cit. on p. 247).
[16] Ulf Norell. “Towards a Practical Programming Language Based on Dependent Type Theory”. PhD Thesis. Chalmers University, 2007 (cit. on p. 247).
[17] Daniel Peebles et al. Copumpkin/Categories. URL: https://github.com/copumpkin/categories (cit. on p. 247).
[18] Marco Perone. Issue: Type Checker Hangs and Errors. Issue 4690. Apr. 18, 2019. URL: https : //github.com/idris-lang/Idris-dev/issues/4690 (cit. on p. 251).
[19] David Reutter and Jamie Vicary. “High-Level Methods for Homotopy Construction in Associative n-Categories”. In: arXiv (Feb. 11, 2019). arXiv: 1902.03831 [math]. (Visited on Apr. 23, 2019) (cit. on p. 247).
[20] David E. Rydeheard and Rod M. Burstall. Computational Category Theory. Prentice Hall Inter-national, 1988. URL: www.cs.man.ac.uk/ david/categories/book/book.ps (cit. on p. 247). · Zbl 0649.18001
[21] Vladimiro Sassone. “On the Category of Petri Net Computations”. In: TAPSOFT ’95: Theory and Practice of Software Development. Ed. by Peter D. Mosses, Mogens Nielsen, and Michael I. Schwartzbach. Red. by Gerhard Goos, Juris Hartmanis, and Jan Leeuwen. Vol. 915. Springer Berlin Heidelberg, 1995, pp. 334-348. DOI: 10.1007/3-540-59293-8_205. (Visited on May 5, 2018) (cit. on p. 246).
[22] Statebox Team. Idris-Ct Github Page. 2019. URL: https://github.com/statebox/idris-ct (cit. on pp. 246, 247).
[23] Statebox Team. Statebox, Compositional Diagrammatic Programming Language. 2017. URL: https://statebox.org (cit. on p. 246).
[24] Statebox Team. “The Mathematical Specification of the Statebox Language”. In: arXiv (June 18, 2019). arXiv: 1906.07629 [cs, math]. (Visited on June 28, 2019) (cit. on p. 246).
[25] Statebox Team. Typedefs Github Page. 2018. URL: http://typedefs.com (cit. on p. 252).
[26] The Coq Consortium. The Coq Proof Assistant. URL: https://coq.inria.fr/ (cit. on p. 247).
[27] Tom Wildenhain. “On the Turing Completeness of MS PowerPoint”. In: The Official Proceed-ings of the Eleventh Annual Intercalary Workshop about Symposium on Robot Dance Party in Celebration of Harry Q Bovik’s 26th Birthday. SIGBOVIK 2017. Lulu, 2017, pp. 102-106. URL: http://www.sigbovik.org/2017/proceedings.pdf (cit. on p. 247).
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.