Uses of $\infty$-categories in TCS I'm not a theoretical computer scientist. I'm a stable homotopy theorist using $\infty$-categories. I've seen applications of category theory and topos theory to theoretical computer science, and I was wondering if there was any way one could use $\infty$-categories (and preferably for me, stable homotopy theory) in theoretical computer science. I think HoTT mught be one such application, but I may very well be wrong because I know close to nothing about HoTT. (So I also don't know how HoTT is used 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 ideas. Even there though, there only have been few applications of category theory of "dimension" higher than 2.

One nice "computer science-y" one is Homotopical Patch Theory by Anguili et al. They show that some common operations and properties inherent git like version control systems can be best understood using homotopy type theory.

Another rather unrelated train of thought is some interesting work on the relationship between (2-)Homology theory and confluence of term rewrite systems (or more complex structures such as higher algebras). Some examples are

Y. Guiraud Confluence of linear rewriting and homology of algebras .

Y. Lafont &amp; A. Proute Church-Rosser property and homology of monoids.