[CarpaDorada]

>Applications of category theory to computer science predate the first US computer science department.

This doesn't sound plausible: according to Wikipedia, Eilenberg and Mac Lane introduced concepts of CT in 1942, and CT was originally used mainly homological algebra, with applications in logic/semantics later. Certainly CT was given credence by Grothendieck and Serre, working on (and solving) Weil's conjecture in the 50s and 60s. Lawvere's 1963 thesis predated categorical logic (according to his own words, <http://www.tac.mta.ca/tac/reprints/articles/5/tr5abs.html> p. 12, "but the method here, and indeed in the whole ensuing categorical logic, is to exploit the uniqueness by using adjointness itself as an axiom"). The first computer science department in the US was started in 1962 in Purdue University. Meanwhile for contrast the proofs of Church and Turing were published in 1936.

>I would wager that you can't name a logic not expressible in category theory.

I prefaced my statement with an "if"; you're not talking about toposes apparently. The interpretability of one theory in another is a concern of logicians and I'm not familiar with any restrictions on category theory, indeed it can be used for logics. I do not know topos theory but I was basing my statement on what I heard Colin McLarty say in an interview of his <https://www.youtube.com/watch?v=81sPQGIWEfM>, can't give timestamp; he definitely named logics that cannot be expressed by the topos of a space.

I feel that you've used two straw men: 1) specifically naming US 2) ignoring my "if topos" and saying "expressible in CT".