While it downloads, speaking about Lambek, in Lambek-Scott they prove the equivalence of CCC's and simply typed lambda calculus. I suffered some functional programming exposure via Lisp, and came later to see that in the core of lisp, the lambdas, were formalized by (you guess it), lambda calculus. This idea migrates also to Haskell, so if one is pressed to give a formal Haskell semantics, that is a good bootstrap. But that is equivalent to CCCs (cartesian closed categories) as per Lambek-Scott, where the essential feature of CCCs is having functions of functions, higher order functions. And that is not just self-pleasure, look at Conal Elliot's "compiling to categories". Applications I think I've heard of: probabilistic programming and automatic differentiation.

Lambek-Scott: Introduction to Higher-Order Categorical Logic

http://conal.net/papers/compiling-to-categories

https://ncatlab.org/nlab/show/automatic+differentiation