Simply typed type theory and computability. Assume that atomic types of simply typed lambda calculus($\lambda\to$) are interpreted as sets.
Does every (total) computable function can be written as term in such calculus?
If no, please give counterexample.
If yes, please give a title of some book to which I can refer to. (I suspect it is something like "Kleene thesis", but I am not sure at all.)
p.s. does exist "standard" reference to some book(monography?) about simple typed lambda calculus which contains all covering this topic?
 A: The answer is no. If by atomic types we mean base type constants without any introduction or elimination rules, then for any base type $A$, the type $A \rightarrow A$ has only the identity function $\lambda x. x$ as closed inhabitant. This follows by induction on normal forms. Hence, if $A$ is interpreted as any set with more than one element, there are computable functions which are not definable as lambda terms.
There is a precise characterization of set-theoretic functions which are definable as STLC terms: these are the functions which preserve all Kripke logical predicates on base types. Here's a nice and modern exposition with an Agda formalization. The idea AFAIK comes from here, but I find that somewhat outdated in terminology and exposition. The key phrase to search for results like this is "lambda definability".
What if we have base types for natural numbers, $\mathsf{Bool}$, etc., with the appropriate introduction and elimination rules? For example, can STLC+$\mathsf{Nat}$ define all computable $\mathbb{N} \rightarrow \mathbb{N}$ functions? The answer is still no. There is no total programming language for all total computable functions, for Gödelian reasons. In particular, no total language implements a self-interpreter, because that could be used to implement general recursion, contradicting totality. This is a folklore result, you can find it e.g. as Theorem 3.2 here.
In the case of STLC+$\mathsf{Nat}$, we have a bit more specific information about definable functions: we know that the proof-theoretic ordinal of this system is $\epsilon_0$, since a) this language is Gödel's System T, and Gödel showed that the definable functions in System T are precisely the functions provably total in Peano Arithmetic b) the proof-theoretic strength of PA is $\epsilon_0$. Therefore $f_{\epsilon_0}$ in the fast-growing hierarchy is an example for a computable $\mathbb{N} \rightarrow \mathbb{N}$ function which is not definable in STLC+$\mathsf{Nat}$, and in fact grows faster than any STLC+$\mathsf{Nat}$-definable function.
