Church's Theory is one of the older type theories (1940) based on (Church's) simply typed lambda calculus, with logical constants added at the appropriate types. It is the basis for lambda-prolog (Miller,Nadathur, Pfenning, Scedrov), as well as Peter Andrews' work on higher-order automated deduction in the 60s and 70s. Its classical semantics was developed in Henkin's thesis in 1950, and an intensional variant by Andrews in the 1970s. Using an indexed version of (Kripke-like) Omega-set models, we develop sound and complete semantics for the intuitionistic fragment of Church's theory of types (ICTT). We then show how to adapt the semantics to the lambda-prolog fragment(HOHH)of this theory via Uniform Algebras, a Goal-Atom-Program sorted variant of the above semantics. The problem of producing sound and complete semantics for Higher Order Hereditarily Harrop formulas with resolution (uniform) proofs had been open for ten years. We have solved it, but have not touched the question of lambda-prolog's rather unique brand of polymorphism or its kind and type definition mechanisms. The mathematical background required is quite basic (a little intuitionistic semantics, an affection for completeness theorems). The work was done jointly with Mary de Marco at Wesleyan.