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 soundne...
| Main Author: | |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
Scientific and Technological Research Council of Turkey (TUBITAK-ULAKBIM)
2022
|