The simply typed lambda calculus has a class of extremely intuitive models where each basic type $\sigma$ is modeled by some set $[\![\sigma]\!]$, and a complex type $\sigma\rightarrow\tau$ is then straightforwardly interpreted as the full function space $[\![\tau]\!]^{[\![\sigma]\!]}$.
It seems like simply typed combinatory logic should have models of exactly the same kind, with each basic combinator getting a fixed uniform interpretation so that it picks out the 'right' object of its type.
It's also well known how to emulate abstraction in combinatory logic, by defining a term $[x].M$ that behaves like $\lambda x. M$ in the sense that $([x].M\ N)\vartriangleright M[N/x]$.
My question is whether or not there is a strong semantic correspondence between $[x].M$ and $\lambda x. M$ in the kind of extremely simple models that I gestured out. I would guess that $[ \! [[x].M]\! ]=[\![ \lambda x. M]\!]$, but I haven't been able to find an explicit discussion of this anywhere.