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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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, ...
user avatar
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(...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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-...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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, ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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, ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 2,637

Only top scored, non community-wiki answers of a minimum length are eligible