I am already implicitly assuming there are no applications in Theory A found so far, but if you have some of those, that's even better for me!
My understanding is that Joyal's theory of species is used relatively widely in enumerative combinatorics, as a generalization of generating functions which additionally tell you how to permute things in addition to how many there are.
Pippenger has applied Stone duality to relate regular languages and varieties of semigroups. Jeandel has introduced topological automata apply these ideas to give unified accounts (and proofs!) for quantum, probabilistic, and ordinary automata.
Roland Backhouse has given abstract characterizations of greedy algorithms by means of Galois connections with the tropical semiring.
In a much more speculative vein, Noam mentioned sheaf models. These abstractly characterize the syntactic technique of logical relations, which is probably one of the most powerful techniques in semantics. We mostly use them to prove inexpressibility and consistency results, but it should be interesting for complexity theorists since it is a nice example of a practical non-natural (in the sense of Razborov/Rudich) proof technique. (However, logical relations are usually very carefully designed to guarantee that they relativize -- as language designers, we want to be able to assure programmers that function calls are black boxes!)
EDIT: I'll continue speculating, at Ryan's request. As I understand it, a natural proof is roughly one along the lines of trying to define an inductive invariant of the structure of a circuit, subject to various sensible conditions. Similar ideas are (unsurprisingly) pretty common in programming languages as well, when you try to define invariant maintained inductively by a lambda-calculus term (for instance, to prove type safety). 1
However, this technique often breaks down at higher (ie, function) types. For example, the simply-typed lambda calculus is total -- every program written in it terminates. However, straightforward attempts to prove this tend to founder on the problem of first-class functions: it's not enough to prove that every term of type $A \to B$ terminates. Since we can additionally apply arguments to functions, we not only need to ensure that every term of type $A \to B$ halts, we also need to ensure that this property holds "hereditarily" -- we also need to know that given any term of type $A$, the application will also halt.
This is what logical relations do. Instead of defining a single inductive invariant, we define a whole family of predicates by recursion over the structure of (typically) the type. Then, we prove that every definable term lies in the appropriate predicate, which lets us establish what we sought. So for termination, we would say that good values of base type are the values of base type, and the good values of type $A \to B$ are the values of this type which, given a good value of $A$, evaluates to a good value of $B$. Note that there is no single inductive invariant -- we define a whole family of invariants by recursion over the structure of the input, and use other means to show that all terms lie within these invariants. Proof-theoretically, this is a vastly stronger technique, and is why it lets you prove consistency results.
The connection to sheaves arises from the fact that we often need to reason about open terms (ie, terms with free variables), and so need to distinguish between getting stuck due to errors and getting stuck due to needing to reduce a variable. Sheaves arise from considering the reductions of the lambda calculus as defining the morphisms of a category whose terms are the objects (ie, the partial order induced by reduction), and then considering the functors from this category into sets (ie, predicates). Jean Gallier wrote some nice papers about this in the early 2000s, but I doubt they are readable unless you have already assimilated a fair amount of lambda calculus.
