Formal categorical reasoning

In this paper, we present a category theory library developed in the proof assistant Coq. We discuss the design principles of the library in comparison with those existing out there. To explicitly demonstrate the utility of the library, we conclude with a case study in which a Coq formalized soundness proof of the intuitionistic propositional logic within a category theoretical settings is examined.

PDF

___

[1] Byliński C. Introduction to categories and functors. Formalized Mathematics,1990: 1(2):409-420.
[2] Capriotti P. pcapriotti/agda-categories at GitHub.
[3] Coq Development Team. The Coq proof assistant reference manual, 2018. Version 8.8.1.
[4] Coquand T, Paulin C. Inductively defined types. In: Martin-Löf P, Mints G (editors). International Conference on Computer Logic, Tallinn, USSR, December 1988, Proceedings, volume 417 of Lecture Notes in Computer Science, pages 50–66. Springer, 1988.
[5] Dowek G, Hardin T, Kirchner C. Higher order unification via explicit substitutions. Information and Computation, 2000; 157(1-2):183-235.
[6] Ekici B. ekiciburak/CatTheo at GitHub.
[7] Ekici B, Kaliszyk C. Mac Lane’s comparison theorem for the Kleisli construction formalized in Coq. Mathematics in Computer Science, Feb 2020. ISSN 1661-8289.
[8] Elliott C. Compiling to categories. Proceedings of the ACM on Programming Languages, 1(ICFP):2017; 27: 1-27:27.
[9] Freire JL, Brañas EF, Blanco A. On recursive functions and well-founded relations in the calculus of constructions. In: Moreno-Díaz R, Pichler F, Quesada-Arencibia A (editors). Computer Aided Systems Theory - EUROCAST 2005, 10th International Conference on Computer Aided Systems Theory, Las Palmas de Gran Canaria, Spain, February 7-11, 2005, Revised Selected Papers, volume 3643 of Lecture Notes in Computer Science, pages 69-80. Springer, 2005.
[10] Gross J, Chlipala A, Spivak DI. Experience implementing a performant category-theory library in Coq. In: Klein G, Gamboa R (editors). Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of LNCS, pages 275–291. Springer, 2014.
[11] Huet GP. Cartesian closed categories and lambda-calculus. In: Cousineau G, Curien P, Robinet B (editors). Combinators and Functional Programming Languages, Thirteenth Spring School of the LITP, Val d’Ajol, France, May 6-10, 1985, Proceedings, volume 242 of Lecture Notes in Computer Science, pages 123–135. Springer, 1985.
[12] Ishii H. konn/category-agda at GitHub.
[13] Lambek J. From λ-calculus to cartesian closed categories. To HB Curry: essays on combinatory logic, lambda calculus and formalism, pages 1980: 375-402.
[14] Lambek J. Cartesian closed categories and typed lambda-calculi. In: Cousineau G, Curien P, Robinet B (editors). Combinators and Functional Programming Languages, Thirteenth Spring School of the LITP, Val d’Ajol, France, May 6-10, 1985, Proceedings, volume 242 of Lecture Notes in Computer Science, pages 136-175. Springer, 1985.
[15] Moggi E. Notions of computation and monads. Information and Computation, 93(1):55–92, July 1991. ISSN 0890-5401.
[16] Peebles D. copumpkin/categories at GitHub.
[17] Pouillard N. crypto-agda/crypto-agda at GitHub.
[18] Spies S, Forster Y. Undecidability of higher-order unification formalised in Coq. In: Blanchette J, Hritcu C (editors). Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 143-157. ACM, 2020.
[19] Timany A, Jacobs B. Category theory in Coq 8.5. In Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, Porto, Portugal, pages 2016; 30: 1-30.
[20] Voevodsky V, Ahrens B, Grayson D, et al. UniMath — a computer-checked library of univalent mathematics.
[21] Wadler P. Monads for functional programming. In: Jeuring J, Meijer E (editors). Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques, Båstad, Sweden, May 24-30, 1995, Tutorial Text, volume 925 of Lecture Notes in Computer Science, pages 24–52. Springer, 1995.
[22] Wiegley J. jwiegley/category-theory at GitHub.