相关论文: idris-ct: A Library to do Category Theory in Idris

This thesis deals with two main topics: virtual double categories as semantics environments for predicate logic, and a syntactic presentation of virtual double categories as a type theory. One significant principle of categorical logic is…

This paper introduces a category theory-based framework to redefine physical computing in light of advancements in quantum computing and non-standard computing systems. By integrating classical definitions within this broader perspective,…

Using the concepts of category and functor, we provide some insights and prove an intrinsic property of the category ${\bf AprS}$ of approximation spaces and relation-preserving functions, the category ${\bf RCls}$ of rough closure spaces…

Category theory provides an alternative to Hilbert's Formal Axiomatic method and goes beyond Mathematical Structuralism

Category theory is the language of homological algebra, allowing us to state broadly applicable theorems and results without needing to specify the details for every instance of analogous objects. However, authors often stray from the realm…

We report on our experience implementing category theory in Coq 8.5. The repository of this development can be found at https://bitbucket.org/amintimany/categories/. This implementation most notably makes use of features, primitive…

Category theory unifies mathematical concepts, aiding comparisons across structures by incorporating objects and morphisms, which capture their interactions. It has influenced areas of computer science such as automata theory, functional…

Software engineering concepts and processes are worthy of formal study; and yet we seldom formalize them. This "research ideas" article explores what a theory of software engineering could and should look like. Software engineering research…

While Chain-of-Thought (CoT) prompting enhances the reasoning capabilities of large language models, the faithfulness of the generated rationales remains an open problem for model interpretability. We propose a novel theoretical lens for…

Cryptography is a theory of secret functions. Category theory is a general theory of functions. Cryptography has reached a stage where its structures often take several pages to define, and its formulas sometimes run from page to page.…

Integrated information theory (IIT) starts from consciousness itself and identifies a set of properties (axioms) that are true of every conceivable experience. The axioms are translated into a set of postulates about the substrate of…

Questions of set-theoretic size play an essential role in category theory, especially the distinction between sets and proper classes (or small sets and large sets). There are many different ways to formalize this, and which choice is made…

The introduction of first-class type classes in the Coq system calls for re-examination of the basic interfaces used for mathematical formalization in type theory. We present a new set of type classes for mathematics and take full advantage…

Classification is an important goal in many branches of mathematics. The idea is to describe the members of some class of mathematical objects, up to isomorphism or other important equivalence in terms of relatively simple invariants. Where…

We introduce basic notions in category theory to type theorists, including comprehension categories, categories with attributes, contextual categories, type categories, and categories with families along with additional discussions that are…

I discuss (ontologies_and_ontological_knowledge_bases / formal_methods_and_theories) duality and its category theory extensions as a step toward a solution to Knowledge-Based Systems Theory. In particular I focus on the example of the…

Research software has been categorized in different contexts to serve different goals. We start with a look at what research software is, before we discuss the purpose of research software categories. We propose a multi-dimensional…

Today, there are millions of professionals worldwide acting as a designer, architect or engineer in the design, realization, and implementation of information systems. At this moment there is no well established and clearly identified body…

The depth-bounded fragment of the pi-calculus is an expressive class of systems enjoying decidability of some important verification problems. Unfortunately membership of the fragment is undecidable. We propose a novel type system,…

We introduce a notion of complexity of diagrams (and in particular of objects and morphisms) in an arbitrary category, as well as a notion of complexity of functors between categories equipped with complexity functions. We discuss several…