Category theory in Isabelle/HOL as a basis for meta-logical investigation

DOI10.1007/978-3-031-42753-4_5arXiv2306.09074OpenAlexW4386297785MaRDI QIDQ6118814

Dana S. Scott, Alexey Gonus, Jonas Bayer, Christoph Benzmüller

Publication date: 28 February 2024

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2306.09074

zbMATH Keywords

category theoryformal methodsformalization of mathematicsproof assistantsshallow embeddings

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
• Automating free logic in HOL, with an experimental application in category theory
• Automating Free Logic in Isabelle/HOL
• Introduction to Categories and Categorical Logic
• Syntactical and semantical properties of simple type theory
• Computer-Supported Exploration of a Categorical Axiomatization of Modeloids
• Set-theoretic foundations
• A partial functions version of Church's simple theory of types
• What Do We Want a Foundation to Do?

This page was built for publication: Category theory in Isabelle/HOL as a basis for meta-logical investigation