Optimising pointer subtraction with 2-adic integers

A basic cartesian closed category alone only gets you the simply-typed λ-calculus, though, which isn't much fun. The untyped λ-calculus is of course incoherent from the C-H perspective, since unrestricted recursion[0] gives you Turing-equivalence, which corresponds to an inconsistent logic; a categorical description would probably be easy but I don't think I've seen one.

More expressive typed λ-calculi such as System F are more interesting from a computer science perspective, but I've not been able to find much material discussing them from a logical or categorical perspective. Instead, most mathematicians would jump straight to something like Coquand's Calculus of Constructions[1], which is (if memory serves me) the internal logic of a topos.

Category theory also sees some use in computer science beyond just C-H stuff--for instance, describing recursive data types as fixed points of endofunctors on the category of types. This permits an elegant categorical description of operations on those types--e.g., the "fold" or "reduce" function on lists is represented by an initial F-algebra. The categorical habit of dualizing everything in reach also pays off: the dual of well-founded recursion collapsing structures using an initial F-algebra is productive corecursion building structures using a terminal F-coalgebra, which turns out to be a useful description of non-terminating programs that compute only on demand and then return to an idle state.

Another fun one: Representing data structures algebraically using sum and product types, it turns out there's a meaningful semantics for taking the derivative of the type--you get the original type with any one value missing, plus enough information to specify the location of the hole.

There's also something involving a relationship between Kan extensions and the continuation-passing transform but that's really getting beyond my knowledge.

I've also seen stuff about running C-H the other way, and using categorical models of linear logic as a semantics for expressing resource awareness and side effects in a programming language.

If you want to see some of the above in action, the ML family of programming languages are based on typed λ-calculi, and acknowledge mathematical connections a bit more that most other languages. Haskell [2] is a more distant cousin in that family, and of the not-completely-obscure languages it tends to most cheerfully play with concepts from category theory. For instance, take a look at some of the material on this blog: http://comonad.com/reader/category/category-theory/ If nothing else, you can probably dig around from Haskell-related material to find more general stuff.

[0] The best-known implementation for recursion is Y, Curry's fixed-point combinator, written in lambda terms as (λf. (λx. f (x x)) (λx. f (x x))). In a typed setting, if it can be expressed at all, it ends up being equivalent via C-H to a proposition (A -> A) -> A, which permits a proof of any proposition. This makes it easy to see how the Halting problem is closely related to Godel's incompleteness theorem, as any language with a coherent interpretation via C-H will reject some perfectly sensible programs (i.e., is incomplete).

[1] The CoC is also the basis for the proof assistant/programming language Coq. See also the "Lambda Cube" for a taxonomy of orthogonal type system enhancements.

[2] Named for Prof. H. Curry, of course.