•  
  •  
 

Turkish Journal of Mathematics

Authors

BURAK EKİCİ

DOI

10.55730/1300-0098.3178

Abstract

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.

First Page

1538

Last Page

1552

Included in

Mathematics Commons

Share

COinS