Formal categorical reasoning

Ekici B.

TURKISH JOURNAL OF MATHEMATICS, cilt.46, sa.4, ss.1538-1554, 2022 (SCI-Expanded) identifier identifier

  • Yayın Türü: Makale / Tam Makale
  • Cilt numarası: 46 Sayı: 4
  • Basım Tarihi: 2022
  • Doi Numarası: 10.3906/mat-2202-126
  • Dergi Adı: TURKISH JOURNAL OF MATHEMATICS
  • Derginin Tarandığı İndeksler: Science Citation Index Expanded (SCI-EXPANDED), Scopus, Academic Search Premier, MathSciNet, zbMATH, TR DİZİN (ULAKBİM)
  • Sayfa Sayıları: ss.1538-1554
  • Anahtar Kelimeler: Categorical logic, denotational semantics of programming constructs, formal proofs, the Coq proof assistant
  • TED Üniversitesi Adresli: Evet

Özet

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.