I am an homotopy theorist, interested in computer science.
I would like to ask what are some interesting applications of homotopical algebra (model categories, infinity categories, simplicial categories, etc) in theoretical computer science?
Two big applications of homotopy theory in theoretical computer science are
Homotopy Type Theory revealed a completely unexpected connection between the theory of the typed lambda calculus and homotopy theory. As a quick intuition, think of it as either a (vast) generalization of the connection between intuitionistic logic and topological spaces, or a language for doing "synthetic homotopy theory".
The directed version of algebraic topology and homotopy theory (ie, where paths are not reversible) has been developed precisely with applications to computer science in mind. The intuition is that the possible evaluations of a concurrent program correspond to a space, program executions correspond to paths in that space, and synchronization primitives correspond to obstructions. By considering the geometric properties of these spaces/programs, it becomes possible to develop tools for reasoning about their behaviour.
The 2004 Gödel Prize was shared by the following two papers:
Quotes from the 2004 Gödel Prize:
The two papers offer one of the most important breakthroughs in the theory of distributed computing.
The discovery of the topological nature of distributed computing provides a new perspective on the area and represents one of the most striking examples, possibly in all of applied mathematics, of the use of topological structures to quantify natural computational phenomena.
A book on this topic: