For my I read a review of Combinatory Categorical Grammar, by Mark Steedman and Jason Baldridge. CCG is a lexicon-heavy formalism (like LFG or HPSG, perhaps) yielding semantics with logical forms (like typed lambda calculus). The expression for a lexical item specifies how it wants to combine with constituents on the left or right. The resulting compositions have their own expressions which can further combine until you have an interpretation for the entire sentence. For example,
Marcel proved completeness
A/B means "combine with right, of type B, yielding A." So [proved completeness] join together to yield
[proved completeness]: S\NP
A\B means "combine with left, of type A, yielding B." So this joins with the left to get
[Marcel [proved completeness]: S
You can also associate lambda calculus expressions with these expressions (I don't know their names), to get the logical forms that we see in the focus paper. There are quite a few more details for how these composition operations work, of course, but there's a core set of principles that seem reasonable.
The review is fairly long (60 pages) and goes over a variety of linguistic phenomena that CCG can handle, and talks a lot about how it relates to other syntactic theories. According to the review, it is the best thing since sliced bread.
I was hoping this would help me understand Section 4 of the focus paper but I'm still confused. I get the impression they only use part of CCG as it's described by Steedman and Baldridge, and then they do something weird too.