Solid applications of category theory in TCS?
I can think of one instance where category theory was directly "applied" to solve an open problem in programming languages: Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Phil Scott, "Normalization by evaluation for typed lambda calculus with coproducts".  From their abstract: "We solve the decision problem for simply typed lambda calculus with strong binary sums, equivalently the word problem for free cartesian closed categories with binary coproducts. Our method is based on the semantical technique known as 'normalization by evaluation' and involves inverting the interpretation of the syntax into a suitable sheaf model and from this extracting appropriate unique normal forms."

In general, though, I think that category theory is not usually applied to prove deep theorems in programming languages (of which there aren't so many), but instead offers a conceptual framework that is often useful (for example in the above, the idea of (pre)sheaf semantics).

An important historical example is Eugenio Moggi's suggestion that the notion of monad (which is basic and ubiquitous in category theory) could be used as part of a semantic explanation of side effects in programming languages (e.g., state, nondeterminism).  This also inspired some reflection on the syntax of programming languages, for example leading directly to the "Monad typeclass" in Haskell (used to encapsulate effects).

More recently (the past decade), this explanation of effects in terms of monads has been revisited from the point of view of the old connection (established by category theorists, in the 60s) between monads and algebraic theories: see Martin Hyland and John Power's, "The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads".  The idea is that the monadic view of effects is compatible with the (in some ways more appealing) algebraic view of effects, wherein effects (e.g., store) can be explained in terms of operations (e.g., "lookup" and "update") and associated equations (e.g., idempotency of update).  There is a recent paper building on this connection by Paul-André Melliès, "Segal condition meets computational effects", which also relies heavily on ideas coming from "higher category theory" (for example the notion of "Yoneda structure" as a way of organizing presheaf semantics).

Another, related class of examples comes from linear logic.  Soon after its introduction by Jean-Yves Girard in the 80s (with an aim of a better understanding of constructive logic), solid connections to category theory were established.  For some explanation of this connection, see John Baez and Mike Stay's, "Physics, Topology, Logic and Computation: A Rosetta Stone".

Finally, this answer would be incomplete without reference to sigfpe's illuminating blog "A Neighborhood of infinity".  In particular you could check out "A Partial Ordering of some Category Theory applied to Haskell".