28
votes
Accepted
Impact of Grothendieck's program on TCS
Grothendieck's inequality, from his days in functional analysis, was initially proved to relate fundamental norms on tensor product spaces. Grothendieck called the inequality "the fundamental theorem ...
- 18k
27
votes
Algebra oriented branch of theoretical computer science
There have been recent developments in dependent type theory which relate type systems to homotopy types.
This is now a relatively small field, but there is a lot of exciting work being done right ...
- 13.2k
25
votes
Algebra oriented branch of theoretical computer science
Algebraic geometry is used heavily in algebraic complexity theory and in particular in geometric complexity theory. Representation theory is also crucial for the latter, but it's even more useful when ...
- 35.7k
19
votes
Impact of Grothendieck's program on TCS
Grothendieck's impact can be felt in type theory and logic. For instance, Bart Jacobs' 700+ page volume Categorical Logic and Type Theory gives a uniform treatment of various type theories ($X$-type ...
- 16.6k
19
votes
Is there a relationship between relational algebra/calculus and category theory?
Categorical approaches to query languages is a bit of a niche interest, but I think it's a very interesting niche!
Two of the key figures in this area are Peter Buneman and Torsten Grust. Obviously, ...
- 31.6k
18
votes
Accepted
Proof relevance vs. proof irrelevance
There are several possible notions of proof relevance. Let us consider three similar situations:
An element of a sum $\Sigma (x : A) . P(x)$ is a pair $(a, p)$ where $a : A$ and $p$ is a proof of $P(...
- 26.6k
17
votes
Status quo of category theory and monads in theoretical computer science research?
There have been a number of developments with regards to the use of monads in the theory of computation since Eugenio Moggi's work. I am not able to give a comprehensive account, but here are some ...
- 26.6k
15
votes
Algebra oriented branch of theoretical computer science
Your knowledge of field theory would be useful in cryptography, while category theory is heavily used in the research on programming languages and typing systems, both of which are closely related to ...
- 10.3k
15
votes
"The" category of Turing machines?
If your objects are Turing machines, there are several reasonable possibilities for morphisms. For example:
1) Consider Turing machines as the automata they are, and consider the usual morphisms of ...
- 35.7k
14
votes
"The" category of Turing machines?
You might be interested in Turing categories by Robin Cockett and Pieter Hofstra. From the point of view of category theory the question "what is the category of Turing machines" is less interesting ...
- 26.6k
14
votes
Does the uncomputability of Kolmogorov complexity follow from Lawvere's Fixed Point Theorem?
EDIT: Adding the caveat that Roger's fixed-point theorem may not be a special case of Lawvere's.
Here is a proof that may be "close"... It uses Roger's fixed-point theorem instead of Lawvere's ...
- 8,143
13
votes
Accepted
Category-theoretic treatment of diffs, patches and merging?
As pointed by Martin, there is some work on the categorical representation of patches. Mimram and Di Giusto's "A Categorical Theory of Patches" being the most extensive categorical approach to edit-...
- 146
13
votes
Proof relevance vs. proof irrelevance
I recommend that everyone first read Andrej Bauer's answer, as he covers all the basics extremely well. I agree with everything he says in his answer. I humbly offer more comments, even though I know ...
- 1,490
12
votes
Impact of Grothendieck's program on TCS
Any applications of $p$-adic cohomology, etale cohomology in point counting formulas for algebraic varieties has roots in his work.
I am guessing Mulmuley's vision of generalization of Riemann ...
- 12.5k
12
votes
Accepted
"The" category of Turing machines?
Saal Hardali mentioned that he wanted a category of Turing machines to do geometry (or at least homotopy theory) on. However, there are a lot of different ways to achieve similar aims.
There is a ...
- 31.6k
11
votes
Algebra oriented branch of theoretical computer science
Field theory and algrebraic geometry would be useful in topics related to error correcting codes, both in the classical setting as well as in studying locally decodable codes and list decoding. I ...
- 18k
11
votes
What's the relation between OOP and category theory?
There are absolutely some relationships between the semantics and practice of OOP and category theory. This is somewhat unsurprising since both fields attempt to give a principled generic account of ...
- 13.2k
11
votes
Accepted
Relating univalence for a theory of cateogries to the skeleton concept
I refer you to Chapter 9 of the HoTT book. In particular, a category is defined in such a way that isomorphic objects are equal, see Definition 9.1.6. As Example 9.1.15 points out, there really isn't ...
- 26.6k
11
votes
Are there knot theoretic formulations of NP complete problems?
You can take a look to:
Peter Golbus, Robert W. McGrail, Tomasz Przytycki, Mary Sharac, and Aleksandar Chakarov. 2009. Tricolorable torus knots are NP-complete. In Proceedings of the 47th Annual ...
- 22.3k
11
votes
Uses of $\infty$-categories in TCS
Applying higher homotopy-theoretic ideas to CS is still a very nascent field! My understanding is that it's not even that old as a mathematical field.
Certainly HoTT is the central impetus for such ...
- 13.2k
11
votes
Uses of $\infty$-categories in TCS
Theoretical computer scientists do many things, one of which is mathematical modeling of various computer-sciency things. For instance, we like to provide mathematical models of programming languages, ...
- 26.6k
11
votes
Accepted
A bicartesian closed category of strict complete partial orders (Hask)
Yes, it's impossible to have a nondegenerate CCC with general recursion and categorical coproducts. The standard reference for this is:
H. Huwig and A. Poigne. A note on inconsistencies caused by ...
- 31.6k
11
votes
Accepted
What kind of theoretical object corresponds to a C++ concept?
From a programming language theory perspective, as opposed to the computability perspective other answers and comments have offered, C++ templates combined with concepts correspond to bounded ...
- 16.6k
11
votes
Accepted
What logic correponds via Curry-Howard to a Monad?
The two papers to look at it are Benton, Bierman and de Paiva's Computational Types from a Logical Perspective, which directly gives a proof theory for Moggi's computational lambda-calculus; and Rowan ...
- 31.6k
10
votes
Is there a concept of something like co-applicative functors sitting between comonads and functors?
In this post on SO I found an interesting answer - decisive functors. If we replace () by Void, ...
- 2,471
10
votes
Accepted
Is there any known CCC closed under a probabilistic powerdomain operation?
The following is an extended comment, it does not answer your question in the terms you posed it but does give a semantics for higher-order probabilistic calculi which you may find of interest.
In ...
- 4,823
9
votes
Accepted
Explaining monad transformers in categorical terms
According to Oleksandr Manzuk, they are "translation of a monad along an adjunction", see "Calculating Monad Transformers with Category Theory". By the way, that's the third hit on Google for "monad ...
- 26.6k
9
votes
Are there knot theoretic formulations of NP complete problems?
There are a few references in the first paragraph of
Marc Lackenby. A polynomial upper bound on Reidemeister moves. arXiv:1302.0180
In particular, the author says that the problem of recognizing ...
- 4,309
9
votes
Accepted
Category theory and parsers --- references wanted
One of the very first applications of category theory to a subject outside of algebraic geometry was to parsing! The keywords you want to guide your search are "Lambek calculus" and "categorial ...
- 31.6k
8
votes
Accepted
Categories a computer scientist should know about
Note that most of the categories you considered are 'abstract', i.e., they require structure or properties of an abstract category. As computer scientists we should also be familiar several concrete ...
- 2,637
Only top scored, non community-wiki answers of a minimum length are eligible