Showing 1–1 of 1 results for author: Gonus, A

Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation

Authors: Jonas Bayer, Aleksey Gonus, Christoph Benzmüller, Dana S. Scott

Abstract: This paper presents meta-logical investigations based on category theory using the proof assistant Isabelle/HOL. We demonstrate the potential of a free logic based shallow semantic embedding of category theory by providing a formalization of the notion of elementary topoi. Additionally, we formalize symmetrical monoidal closed categories expressing the denotational semantic model of intuitionistic… ▽ More This paper presents meta-logical investigations based on category theory using the proof assistant Isabelle/HOL. We demonstrate the potential of a free logic based shallow semantic embedding of category theory by providing a formalization of the notion of elementary topoi. Additionally, we formalize symmetrical monoidal closed categories expressing the denotational semantic model of intuitionistic multiplicative linear logic. Next to these meta-logical-investigations, we contribute to building an Isabelle category theory library, with a focus on ease of use in the formalization beyond category theory itself. This work paves the way for future formalizations based on category theory and demonstrates the power of automated reasoning in investigating meta-logical questions. △ Less

Submitted 16 June, 2023; v1 submitted 15 June, 2023; originally announced June 2023.

Comments: 15 pages. Preprint of paper accepted for CICM 2023 conference

MSC Class: 68T15; 03B35; 03B80; 03B15; 08A05; 03C10; 03C68; 03C75; 20B05; 54H20 ACM Class: F.4; I.2.3

Journal ref: Intelligent Computer Mathematics (CICM 2023). Lecture Notes in Computer Science, vol 14101, pp. 69-83. Springer, Cham